Re: I am trying to figure out...

Adam:

>> There are two user-defined sets A and B. The first theorem to be proved is:
>>
>>    for a,A being set st a being Element of A holds a in A;      ::Q1
>
> It holds if (and only if) A is non-empty.

If Mizar's type system wasn't broken (in the sense that
it doesn't allow types to be empty; well, maybe "broken"
is too strong a word, but the Mizar type system _is_
severly limited because of this) then one could define
"Element of" in the natural way.  And then this would be
a provable theorem (and then in fact it would be automatic
when one has requirement SUBSET, I guess.)

Freek