Re: [mizar] structures

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Tue, 8 Oct 2002, Andrzej Trybulec wrote:

> Grzegorz (Bancerek) propose that we should adopt an additional rule, that
>     'the fixed set' should be the empty set
> I agree, but it looks as a requirement. Moreover, he proposed that if the
> empty set has the type theta, then 'the fixed theta' equals to the empty set.
> It may be generalized: if the mother type of theta is theta_1 and
>       the theta is theta_1
> then
>      the theta = the theta_1

If I understand this correctly, recursion (ending at the top of the type 
hierarchy, i.e. "set") gives for all types "the theta" = "the fixed set".

Josef