theorem Th39: :: SURREAL0:39
for A, B being Ordinal
for a, b being object st a <= No_Ord A,b & a in Day B & b in Day B holds
a <= No_Ord B,b