let X1, X2, Y1, Y2 be surreal-membered set ; :: thesis: ( X2 <=_ X1 & Y2 <=_ Y1 & [X1,Y1] is surreal implies [X2,Y2] is surreal )
assume A1: ( X2 <=_ X1 & Y2 <=_ Y1 & [X1,Y1] is surreal ) ; :: thesis: [X2,Y2] is surreal
A2: X2 << Y2

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in X2 or not r in Y2 or not r <= l )
assume A3: ( l in X2 & r in Y2 ) ; :: thesis: not r <= l
consider l1, l2 being Surreal such that
A4: ( l1 in X1 & l2 in X1 & l1 <= l & l <= l2 ) by A3, A1;
consider r1, r2 being Surreal such that
A5: ( r1 in Y1 & r2 in Y1 & r1 <= r & r <= r2 ) by A3, A1;
( X1 = L_ [X1,Y1] & L_ [X1,Y1] << R_ [X1,Y1] & R_ [X1,Y1] = Y1 ) by A1, SURREAL0:45;
then l < r1 by A4, A5, SURREALO:4;
hence not r <= l by A5, SURREALO:4; :: thesis: verum

end;

consider M being Ordinal such that
A6: for o being object st o in X2 \/ Y2 holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
[X2,Y2] in Day M by A6, A2, SURREAL0:46;
hence [X2,Y2] is surreal ; :: thesis: verum