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

One more thing: this cannot be a fixed rule users could rely on, since the 
"is" statement can generally be undecidable. Just a rule of thumb.

Josef