theorem Th40: :: SURREAL0:40

for x, y being Surreal holds
( x <= y iff for A being Ordinal st x in Day A & y in Day A holds
x <= No_Ord A,y )