Re: [mizar] structures

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

> 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?
>

Yes. "the fixed non empty set". I do not know which one is choice.
Everything proved must be true
for any choice of such a set.
That does not mean that it is impossible to develop a requirement, that
makes it e.g. {{}}. But it must be done by
the implementators, not a user.

>
> 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.
>

I am not certain if we need this.

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

It cannot be related to the proof of a registration of an existential
cluster,
proofs are not exported, and then not imported either.

Greetings,
Andrzej