:: deftheorem Def7 defines Sequence-like ORDINAL1:def 7 :
for IT being set holds
( IT is Sequence-like iff ( proj1 IT is epsilon-transitive & proj1 IT is epsilon-connected ) );