theorem Th15: :: SURREAL0:15

for A, B being Ordinal
for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
ClosedProd (R,A,B) = ClosedProd (S,A,B)