theorem Th26: :: SURREAL0:26

for A, B being Ordinal
for R being Relation st R preserves_No_Comparison_on OpenProd (R,A,B) & R c= OpenProd (R,A,B) holds
ex S being Relation st
( R c= S & S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) )