theorem :: SURREAL0:44

for x, y being Surreal
for X1, X2, Y1, Y2 being set st ( for x being Surreal st x in X1 holds
ex y being Surreal st
( y in X2 & x <= y ) ) & ( for x being Surreal st x in Y2 holds
ex y being Surreal st
( y in Y1 & y <= x ) ) & x = [X1,Y1] & y = [X2,Y2] holds
x <= y