:: deftheorem defines ordinal ORDINAL1:def 4 :
for IT being object holds
( IT is ordinal iff IT is epsilon-transitive epsilon-connected set );