Re: [mizar] Once more: empty types

[Freek Wiedijk <freek@cs.ru.nl>]

Dear Andrzej,

>Somebody asked me how many times
>
>     consider x being theta;
>
>is used in MML. It is 2960 in 566 articles. Some Authors like
>it, e.g. Josef Urban.

Ha!  _I_ like it too!

And you could even write it for possibly empty types theta.
(You just would need a then at the end of the previous line :-))

For instance you might want to write (with theta being the
possibly empty version of "Element of"):

      assume A <> {}; then
      consider x being Element of A;

(In fact I think that I already wrote that today :-))

Now that I write this again, I start wondering:  Maybe this
needs a "by XBOOLE_0:def 1" as well.  I'm not sure.  What do
you think?

Freek