theorem Th22: :: SURREAL0:22

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,0)) = S /\ (OpenProd (S,A,0)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))