theorem Th24: :: SURREAL0:24

for Lp, Lr being Sequence st dom Lp = dom Lr & ( for A being Ordinal st A in dom Lp holds
( ex a, b being Ordinal ex R being Relation st
( R = Lr . A & Lp . A = ClosedProd (R,a,b) ) & Lr . A is Relation & ( for R being Relation st R = Lr . A holds
( R preserves_No_Comparison_on Lp . A & R c= Lp . A ) ) ) ) holds
( union (rng Lr) is Relation & ( for R being Relation st R = union (rng Lr) holds
( R preserves_No_Comparison_on union (rng Lp) & R c= union (rng Lp) & ( for A, a, b being Ordinal
for S being Relation st A in dom Lp & S = Lr . A & Lp . A = ClosedProd (S,a,b) holds
R /\ [:(BeforeGames a),(BeforeGames a):] = S /\ [:(BeforeGames a),(BeforeGames a):] ) ) ) )