let X1, X2, Y1, Y2 be set ; :: thesis: ( X1 <=_ X2 & Y1 <=_ Y2 implies X1 \/ Y1 <=_ X2 \/ Y2 )
assume A1: ( X1 <=_ X2 & Y1 <=_ Y2 ) ; :: thesis: X1 \/ Y1 <=_ X2 \/ Y2
let x be Surreal; :: according to SURREALO:def 3 :: thesis: ( x in X1 \/ Y1 implies ex y1, y2 being Surreal st
( y1 in X2 \/ Y2 & y2 in X2 \/ Y2 & y1 <= x & x <= y2 ) )
assume A2: x in X1 \/ Y1 ; :: thesis: ex y1, y2 being Surreal st
( y1 in X2 \/ Y2 & y2 in X2 \/ Y2 & y1 <= x & x <= y2 )

per cases ( x in X1 or x in Y1 ) by A2, XBOOLE_0:def 3;

suppose x in X1 ; :: thesis: ex y1, y2 being Surreal st
( y1 in X2 \/ Y2 & y2 in X2 \/ Y2 & y1 <= x & x <= y2 )

then consider x2, x3 being Surreal such that
A3: ( x2 in X2 & x3 in X2 & x2 <= x & x <= x3 ) by A1;
take x2 ; :: thesis: ex y2 being Surreal st
( x2 in X2 \/ Y2 & y2 in X2 \/ Y2 & x2 <= x & x <= y2 )
take x3 ; :: thesis: ( x2 in X2 \/ Y2 & x3 in X2 \/ Y2 & x2 <= x & x <= x3 )
thus ( x2 in X2 \/ Y2 & x3 in X2 \/ Y2 & x2 <= x & x <= x3 ) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in Y1 ; :: thesis: ex y1, y2 being Surreal st
( y1 in X2 \/ Y2 & y2 in X2 \/ Y2 & y1 <= x & x <= y2 )

then consider y2, y3 being Surreal such that
A4: ( y2 in Y2 & y3 in Y2 & y2 <= x & x <= y3 ) by A1;
take y2 ; :: thesis: ex y2 being Surreal st
( y2 in X2 \/ Y2 & y2 in X2 \/ Y2 & y2 <= x & x <= y2 )
take y3 ; :: thesis: ( y2 in X2 \/ Y2 & y3 in X2 \/ Y2 & y2 <= x & x <= y3 )
thus ( y2 in X2 \/ Y2 & y3 in X2 \/ Y2 & y2 <= x & x <= y3 ) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

end;