theorem Th34: :: SURREAL0:34

for A, B being Ordinal st A c= B holds
No_Ord A = (No_Ord B) /\ (ClosedProd ((No_Ord B),A,A))