theorem Th20: :: SURREAL0:20

for A, B being Ordinal
for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) holds
R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):]