:: deftheorem defines preserves_No_Comparison_on SURREAL0:def 11 :
for X, R being set holds
( R preserves_No_Comparison_on X iff for a, b being object st [a,b] in X holds
( a <= R,b iff ( L_ a << R,{b} & {a} << R, R_ b ) ) );