theorem :: ORDINAL4:33

for W being Universe holds
( 0-element_of W = {} & 1-element_of W = 1 ) ;