Re: 'element'

Cytowanie Jesse Alama <[email protected]>:

> Can we please change the name of new 'element' subtype of 'set'?

It is the other way around: 'set' is a subtype of 'element'.
>
> To my mind, calling the new subtype 'element' misleadingly suggests  
> that Mizar is making a foundational distinction between sets and  
> urelements.  But that's not the case because TARSKI:1 effectively  
> identifies 'set' and 'element'.
>

An this is the reason that we use 'element' not 'urelement'. On the other hand
'elements' sometimes mimick 'urelements'. The crucial revision, still  
pending, is:
       mode Element of X -> element

also in the case od X being 1-sorted.

> How about 'thing', 'object', or 'item'?

I see no strong arguments for changing notation. I do not see strong  
arguments for 'element', either.

Regards,
Andrzej