Can we please change the name of new 'element' subtype of 'set'?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'.
How about 'thing', 'object', or 'item'? Jesse