Re: [mizar] Private DB

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

Hi Josef,

>a parameterized Mizar type, who generally does not have to be
>non empty for all instantiations of the parameters.

To repeat myself for the _nth_ time (I cannot restrain myself):
_the_ natural mode that has this property is (tada!)

	Element of

I still find it very strange to allow the number zero (how many
centuries did it take people to see the point of that), to allow
empty sets, but not to allow empty types.

Freek