:: deftheorem Def14 defines OSV@ ORDINAL6:def 14 :
for x being set holds
( ( x is Ordinal-Sequence-valued Sequence implies OSV@ x = x ) & ( x is not Ordinal-Sequence-valued Sequence implies OSV@ x = the Ordinal-Sequence-valued Sequence ) );