:: deftheorem defines 0-element_of ORDINAL4:def 2 :
for W being Universe holds 0-element_of W = {} ;