theorem Th31: :: SURREAL0:31

for A, B, X being Ordinal st X c= A & X c= B holds
(No_Ord A) /\ [:(BeforeGames X),(BeforeGames X):] = (No_Ord B) /\ [:(BeforeGames X),(BeforeGames X):]