:: deftheorem Def13 defines OS@ ORDINAL6:def 13 :
for x being set holds
( ( x is Ordinal-Sequence implies OS@ x = x ) & ( x is not Ordinal-Sequence implies OS@ x = the Ordinal-Sequence ) );