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