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: ( not x in X1 ++ Y1 or ex b₁, b₂ being set st
( b₁ in X2 ++ Y2 & b₂ in X2 ++ Y2 & b₁ <= x & x <= b₂ ) )
assume A2: x in X1 ++ Y1 ; :: thesis: ex b₁, b₂ being set st
( b₁ in X2 ++ Y2 & b₂ in X2 ++ Y2 & b₁ <= x & x <= b₂ )
consider x1, y1 being Surreal such that
A3: ( x1 in X1 & y1 in Y1 & x = x1 + y1 ) by A2, Def8;
consider x2, x3 being Surreal such that
A4: ( x2 in X2 & x3 in X2 & x2 <= x1 & x1 <= x3 ) by A3, A1;
consider y2, y3 being Surreal such that
A5: ( y2 in Y2 & y3 in Y2 & y2 <= y1 & y1 <= y3 ) by A3, A1;
take z2 = x2 + y2; :: thesis: ex b₁ being set st
( z2 in X2 ++ Y2 & b₁ in X2 ++ Y2 & z2 <= x & x <= b₁ )
take z3 = x3 + y3; :: thesis: ( z2 in X2 ++ Y2 & z3 in X2 ++ Y2 & z2 <= x & x <= z3 )
( x2 + y2 <= x1 + y2 & x1 + y2 <= x1 + y1 & x1 + y1 <= x3 + y1 & x3 + y1 <= x3 + y3 ) by A4, A5, Th32;
hence ( z2 in X2 ++ Y2 & z3 in X2 ++ Y2 & z2 <= x & x <= z3 ) by A4, A5, Def8, A3, SURREALO:4; :: thesis: verum