Re: [mizar] structures

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

Dear Andrzej,

>Not at all. You have to be certain that the fixed set is
>theta. If we chose the empty set for the fixed set, as
>Grzegorz proposed, then the non empty set must be something
>different, mustn't it?

When you say "the non empty set" you mean "the fixed non
empty set", right?  So which set would that be?

Would it follow from the proof of the correctness condition
of the cluster "cluster non empty set"?  In that case it
would be {{}} (which is equal to 1), I suppose.  Because in
the existence proof in XBOOLE_0, because the "consider x"
would give the fixed set, I suppose.

But if there were more than one cluster for "non empty set",
would "the fixed non empty set" depend on which cluster you
imported?

Freek