:: deftheorem defines 1-element_of ORDINAL4:def 3 :
for W being Universe holds 1-element_of W = 1;