let x, y be Surreal; :: thesis: ( L_ y << {x} & {x} << R_ y implies [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] is Surreal )
assume A1: ( L_ y << {x} & {x} << R_ y ) ; :: thesis: [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] is Surreal
consider A being Ordinal such that
A2: x in Day A by SURREAL0:def 14;
consider B being Ordinal such that
A3: y in Day B by SURREAL0:def 14;
set X = (L_ x) \/ (L_ y);
set Y = (R_ x) \/ (R_ y);
A4: x = [(L_ x),(R_ x)] ;
then A5: L_ x << R_ x by A2, SURREAL0:46;
A6: y = [(L_ y),(R_ y)] ;
then A7: L_ y << R_ y by A3, SURREAL0:46;
A8: x in {x} by TARSKI:def 1;
A9: (L_ x) \/ (L_ y) << (R_ x) \/ (R_ y)

proof

let x1, y1 be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x1 in (L_ x) \/ (L_ y) or not y1 in (R_ x) \/ (R_ y) or not x1 >= y1 )
assume ( x1 in (L_ x) \/ (L_ y) & y1 in (R_ x) \/ (R_ y) ) ; :: thesis: not x1 >= y1

per cases then ( ( x1 in L_ x & y1 in R_ x ) or ( x1 in L_ y & y1 in R_ y ) or ( x1 in L_ x & y1 in R_ y ) or ( x1 in L_ y & y1 in R_ x ) ) by XBOOLE_0:def 3;

suppose ( x1 in L_ x & y1 in R_ x ) ; :: thesis: not x1 >= y1

hence not x1 >= y1 by A5; :: thesis: verum

end;

suppose ( x1 in L_ y & y1 in R_ y ) ; :: thesis: not x1 >= y1

hence not x1 >= y1 by A7; :: thesis: verum

end;

suppose A10: ( x1 in L_ x & y1 in R_ y ) ; :: thesis: not x1 >= y1

then A11: ( x <= y1 & not x >= y1 ) by A8, A1;
L_ x << {x} by Th11;
hence not x1 >= y1 by A8, A10, A11, Th4; :: thesis: verum

end;

suppose A12: ( x1 in L_ y & y1 in R_ x ) ; :: thesis: not x1 >= y1

then A13: ( x1 <= x & not x1 >= x ) by A8, A1;
{x} << R_ x by Th11;
hence not x1 >= y1 by A8, A12, A13, Th4; :: thesis: verum

end;

end;

end;

for x being object st x in ((L_ x) \/ (L_ y)) \/ ((R_ x) \/ (R_ y)) holds
ex O being Ordinal st
( O in A \/ B & x in Day O )

proof

let z be object ; :: thesis: ( z in ((L_ x) \/ (L_ y)) \/ ((R_ x) \/ (R_ y)) implies ex O being Ordinal st
( O in A \/ B & z in Day O ) )
assume z in ((L_ x) \/ (L_ y)) \/ ((R_ x) \/ (R_ y)) ; :: thesis: ex O being Ordinal st
( O in A \/ B & z in Day O )
then ( z in (L_ x) \/ (L_ y) or z in (R_ x) \/ (R_ y) ) by XBOOLE_0:def 3;

per cases then ( z in L_ x or z in R_ x or z in L_ y or z in R_ y ) by XBOOLE_0:def 3;

suppose ( z in L_ x or z in R_ x ) ; :: thesis: ex O being Ordinal st
( O in A \/ B & z in Day O )

then z in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
then consider O being Ordinal such that
A14: ( O in A & z in Day O ) by A4, A2, SURREAL0:46;
O in A \/ B by A14, XBOOLE_0:def 3;
hence ex O being Ordinal st
( O in A \/ B & z in Day O ) by A14; :: thesis: verum

end;

suppose ( z in L_ y or z in R_ y ) ; :: thesis: ex O being Ordinal st
( O in A \/ B & z in Day O )

then z in (L_ y) \/ (R_ y) by XBOOLE_0:def 3;
then consider O being Ordinal such that
A15: ( O in B & z in Day O ) by A3, A6, SURREAL0:46;
O in A \/ B by A15, XBOOLE_0:def 3;
hence ex O being Ordinal st
( O in A \/ B & z in Day O ) by A15; :: thesis: verum

end;

end;

end;

then [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] in Day (A \/ B) by SURREAL0:46, A9;
hence [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] is Surreal ; :: thesis: verum