theorem :: SURREAL0:14

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