Re: [mizar] Why do Mizar types have to be non-empty?

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

Dear Andrzej,

>> So what is the meaning of "n is Normal_form of R" when this
>> "Z" condition fails?

>Then if the 'Z' condition fails, it equals to the fixed (in the game
>theoretic setting - fixed by the opponent, not the proponent) element
>of  (the denotation of) 'theta of R'.

I see.  Does this mean that if R fails the "Z" condition, and
if both n is Normal_form of R and n' is Normal_form of R, that then
n = n'?

Freek