[mizar] Urelements?

[trybulec@math.uwb.edu.pl]

Let me make one thing clear:

we do not propose to chang the foundations of MML. The chang eis rather 
related to type handling.

The (quite old/brand new) TARSKI:1 will be

for x being element holds x is set


It now obvious that 2 is a set, I mean

     2 is set;

is accepted without any references. In new approach it will need 
justification:

     2 is set by TARSKI:1;

I used many times (and it must be revised)

     1-sorted(#1, ... #)

for 1-element 1-sorted. I even wanted to do a revision :-). With new approach
one must write

     1-sorted(#{0}, ...#)

that means the same and it less tricky.

Regards,
Andrzej