theorem Th27: :: SURREAL0:27

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