:: deftheorem Def12 defines No_Ord SURREAL0:def 12 :
for A being Ordinal
for b₂ being Relation holds
( b₂ = No_Ord A iff ( b₂ preserves_No_Comparison_on [:(Day (b₂,A)),(Day (b₂,A)):] & b₂ c= [:(Day (b₂,A)),(Day (b₂,A)):] ) );