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