defpred S₁[ Ordinal] means ( ( for x, y being Surreal st (born x) (+) (born y) c= $1 holds
( x + y is surreal & x + y in Day ((born x) (+) (born y)) ) ) & ( for x, y, z, xz, yz being Surreal st (born x) (+) (born z) c= $1 & (born y) (+) (born z) c= $1 & xz = x + z & yz = y + z holds
( xz <= yz iff x <= y ) ) );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
thus for x, y being Surreal st (born x) (+) (born y) c= D holds
( x + y is surreal & x + y in Day ((born x) (+) (born y)) ) :: thesis: for x, y, z, xz, yz being Surreal st (born x) (+) (born z) c= D & (born y) (+) (born z) c= D & xz = x + z & yz = y + z holds
( xz <= yz iff x <= y )

proof

let x, y be Surreal; :: thesis: ( (born x) (+) (born y) c= D implies ( x + y is surreal & x + y in Day ((born x) (+) (born y)) ) )
assume A3: (born x) (+) (born y) c= D ; :: thesis: ( x + y is surreal & x + y in Day ((born x) (+) (born y)) )
set Bx = born x;
set By = born y;
set B = (born x) (+) (born y);
A4: ( x in Day (born x) & y in Day (born y) ) by SURREAL0:def 18;
( x = [(L_ x),(R_ x)] & y = [(L_ y),(R_ y)] ) ;
then A5: ( L_ x << R_ x & L_ y << R_ y ) by SURREAL0:46, A4;
A6: (L_ x) ++ {y} << (R_ x) ++ {y}

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in (L_ x) ++ {y} or not r in (R_ x) ++ {y} or not r <= l )
assume A7: ( l in (L_ x) ++ {y} & r in (R_ x) ++ {y} ) ; :: thesis: not r <= l
consider l1, l2 being Surreal such that
A8: ( l1 in L_ x & l2 in {y} & l = l1 + l2 ) by A7, Def8;
consider r1, r2 being Surreal such that
A9: ( r1 in R_ x & r2 in {y} & r = r1 + r2 ) by A7, Def8;
A10: ( l2 = y & y = r2 ) by A8, A9, TARSKI:def 1;
set bl = born l1;
set br = born r1;
set bb = (born l1) \/ (born r1);
set B = ((born l1) \/ (born r1)) (+) (born y);
( l1 in (L_ x) \/ (R_ x) & r1 in (L_ x) \/ (R_ x) ) by A8, A9, XBOOLE_0:def 3;
then ( born l1 in born x & born r1 in born x ) by SURREALO:1;
then (born l1) \/ (born r1) in born x by ORDINAL3:12;
then A11: ((born l1) \/ (born r1)) (+) (born y) in (born x) (+) (born y) by ORDINAL7:94;
A12: (born l1) (+) (born y) c= ((born l1) \/ (born r1)) (+) (born y) by ORDINAL7:95, XBOOLE_1:7;
A13: (born r1) (+) (born y) c= ((born l1) \/ (born r1)) (+) (born y) by ORDINAL7:95, XBOOLE_1:7;
l1 < r1 by A8, A9, A5;
hence l < r by A3, A8, A9, A10, A11, A12, A13, A2; :: thesis: verum

end;

A14: ( L_ x << {x} & {x} << R_ x & L_ y << {y} & {y} << R_ y ) by SURREALO:11;
A15: {x} ++ (L_ y) << (R_ x) ++ {y}

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {x} ++ (L_ y) or not r in (R_ x) ++ {y} or not r <= l )
assume A16: ( l in {x} ++ (L_ y) & r in (R_ x) ++ {y} ) ; :: thesis: not r <= l
consider l1, l2 being Surreal such that
A17: ( l1 in {x} & l2 in L_ y & l = l1 + l2 ) by A16, Def8;
consider r1, r2 being Surreal such that
A18: ( r1 in R_ x & r2 in {y} & r = r1 + r2 ) by A16, Def8;
A19: ( l1 = x & r2 = y ) by A17, A18, TARSKI:def 1;
A20: ( l2 in (L_ y) \/ (R_ y) & r1 in (L_ x) \/ (R_ x) ) by A17, A18, XBOOLE_0:def 3;
then ( (born r1) (+) (born l2) in (born x) (+) (born l2) & (born x) (+) (born l2) in (born x) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then A21: (born r1) (+) (born l2) in D by A3, ORDINAL1:10;
then reconsider rl = r1 + l2, lr = l2 + r1 as Surreal by A2;
(born l1) (+) (born l2) in (born x) (+) (born y) by A20, SURREALO:1, A19, ORDINAL7:94;
then A22: (born l1) (+) (born l2) in D by A3;
set B1 = ((born r1) (+) (born l2)) \/ ((born l1) (+) (born l2));
A23: ((born r1) (+) (born l2)) \/ ((born l1) (+) (born l2)) in D by A21, A22, ORDINAL3:12;
A24: (born l1) (+) (born l2) c= ((born r1) (+) (born l2)) \/ ((born l1) (+) (born l2)) by XBOOLE_1:7;
A25: (born r1) (+) (born l2) c= ((born r1) (+) (born l2)) \/ ((born l1) (+) (born l2)) by XBOOLE_1:7;
l1 < r1 by A18, A14, A17;
then A26: l < rl by A17, A24, A25, A23, A2;
(born r1) (+) (born r2) in (born x) (+) (born y) by A20, SURREALO:1, A19, ORDINAL7:94;
then A27: (born r1) (+) (born r2) in D by A3;
set B2 = ((born r1) (+) (born l2)) \/ ((born r1) (+) (born r2));
A28: ((born r1) (+) (born l2)) \/ ((born r1) (+) (born r2)) in D by A21, A27, ORDINAL3:12;
A29: (born r1) (+) (born r2) c= ((born r1) (+) (born l2)) \/ ((born r1) (+) (born r2)) by XBOOLE_1:7;
A30: (born r1) (+) (born l2) c= ((born r1) (+) (born l2)) \/ ((born r1) (+) (born r2)) by XBOOLE_1:7;
A31: l2 < r2 by A18, A14, A17;
assume r <= l ; :: thesis: contradiction
then r <= rl by A26, SURREALO:4;
hence contradiction by A18, A29, A30, A28, A2, A31; :: thesis: verum

end;

A32: (L_ x) ++ {y} << {x} ++ (R_ y)

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in (L_ x) ++ {y} or not r in {x} ++ (R_ y) or not r <= l )
assume A33: ( l in (L_ x) ++ {y} & r in {x} ++ (R_ y) ) ; :: thesis: not r <= l
consider l1, l2 being Surreal such that
A34: ( l1 in L_ x & l2 in {y} & l = l1 + l2 ) by A33, Def8;
consider r1, r2 being Surreal such that
A35: ( r1 in {x} & r2 in R_ y & r = r1 + r2 ) by A33, Def8;
A36: ( l2 = y & r1 = x ) by A34, A35, TARSKI:def 1;
A37: ( r2 in (L_ y) \/ (R_ y) & l1 in (L_ x) \/ (R_ x) ) by A34, A35, XBOOLE_0:def 3;
then ( (born l1) (+) (born r2) in (born x) (+) (born r2) & (born x) (+) (born r2) in (born x) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then A38: (born l1) (+) (born r2) in D by A3, ORDINAL1:10;
then reconsider lr = l1 + r2, rl = r2 + l1 as Surreal by A2;
(born r1) (+) (born r2) in (born x) (+) (born y) by A37, SURREALO:1, A36, ORDINAL7:94;
then A39: (born r1) (+) (born r2) in D by A3;
set B1 = ((born l1) (+) (born r2)) \/ ((born r1) (+) (born r2));
A40: ((born l1) (+) (born r2)) \/ ((born r1) (+) (born r2)) in D by A38, A39, ORDINAL3:12;
A41: (born r1) (+) (born r2) c= ((born l1) (+) (born r2)) \/ ((born r1) (+) (born r2)) by XBOOLE_1:7;
A42: (born l1) (+) (born r2) c= ((born l1) (+) (born r2)) \/ ((born r1) (+) (born r2)) by XBOOLE_1:7;
l1 < r1 by A35, A14, A34;
then A43: lr < r by A35, A41, A42, A40, A2;
(born l1) (+) (born l2) in (born x) (+) (born y) by A37, SURREALO:1, A36, ORDINAL7:94;
then A44: (born l1) (+) (born l2) in D by A3;
set B2 = ((born l1) (+) (born r2)) \/ ((born l1) (+) (born l2));
A45: ((born l1) (+) (born r2)) \/ ((born l1) (+) (born l2)) in D by A38, A44, ORDINAL3:12;
A46: (born l1) (+) (born l2) c= ((born l1) (+) (born r2)) \/ ((born l1) (+) (born l2)) by XBOOLE_1:7;
A47: (born l1) (+) (born r2) c= ((born l1) (+) (born r2)) \/ ((born l1) (+) (born l2)) by XBOOLE_1:7;
A48: l2 < r2 by A35, A14, A34;
assume r <= l ; :: thesis: contradiction
then lr <= l by A43, SURREALO:4;
hence contradiction by A34, A46, A47, A45, A2, A48; :: thesis: verum

end;

A49: {x} ++ (L_ y) << {x} ++ (R_ y)

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {x} ++ (L_ y) or not r in {x} ++ (R_ y) or not r <= l )
assume A50: ( l in {x} ++ (L_ y) & r in {x} ++ (R_ y) ) ; :: thesis: not r <= l
consider l1, l2 being Surreal such that
A51: ( l1 in {x} & l2 in L_ y & l = l1 + l2 ) by A50, Def8;
consider r1, r2 being Surreal such that
A52: ( r1 in {x} & r2 in R_ y & r = r1 + r2 ) by A50, Def8;
A53: ( l1 = x & x = r1 ) by A51, A52, TARSKI:def 1;
set bl = born l2;
set br = born r2;
set bb = (born l2) \/ (born r2);
set B = ((born l2) \/ (born r2)) (+) (born x);
( l2 in (L_ y) \/ (R_ y) & r2 in (L_ y) \/ (R_ y) ) by A51, A52, XBOOLE_0:def 3;
then ( born l2 in born y & born r2 in born y ) by SURREALO:1;
then (born l2) \/ (born r2) in born y by ORDINAL3:12;
then A54: ((born l2) \/ (born r2)) (+) (born x) in (born y) (+) (born x) by ORDINAL7:94;
A55: (born l2) (+) (born x) c= ((born l2) \/ (born r2)) (+) (born x) by ORDINAL7:95, XBOOLE_1:7;
A56: (born r2) (+) (born x) c= ((born l2) \/ (born r2)) (+) (born x) by ORDINAL7:95, XBOOLE_1:7;
l2 < r2 by A51, A52, A5;
hence l < r by A51, A52, A53, A54, A3, A55, A56, A2; :: thesis: verum

end;

A57: ((L_ x) ++ {y}) \/ ({x} ++ (L_ y)) << ((R_ x) ++ {y}) \/ ({x} ++ (R_ y))

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in ((L_ x) ++ {y}) \/ ({x} ++ (L_ y)) or not r in ((R_ x) ++ {y}) \/ ({x} ++ (R_ y)) or not r <= l )
assume ( l in ((L_ x) ++ {y}) \/ ({x} ++ (L_ y)) & r in ((R_ x) ++ {y}) \/ ({x} ++ (R_ y)) ) ; :: thesis: not r <= l
then ( ( l in (L_ x) ++ {y} or l in {x} ++ (L_ y) ) & ( r in (R_ x) ++ {y} or r in {x} ++ (R_ y) ) ) by XBOOLE_0:def 3;
hence not r <= l by A6, A15, A32, A49; :: thesis: verum

end;

for z being object st z in (((L_ x) ++ {y}) \/ ({x} ++ (L_ y))) \/ (((R_ x) ++ {y}) \/ ({x} ++ (R_ y))) holds
ex O being Ordinal st
( O in (born x) (+) (born y) & z in Day O )

proof

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

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

suppose ( z in (L_ x) ++ {y} or z in (R_ x) ++ {y} ) ; :: thesis: ex O being Ordinal st
( O in (born x) (+) (born y) & z in Day O )

then ( ex u, w being Surreal st
( u in L_ x & w in {y} & z = u + w ) or ex u, w being Surreal st
( u in R_ x & w in {y} & z = u + w ) ) by Def8;
then consider u, w being Surreal such that
A58: ( ( u in L_ x or u in R_ x ) & w in {y} & z = u + w ) ;
u in (L_ x) \/ (R_ x) by A58, XBOOLE_0:def 3;
then ( born u in born x & w = y ) by A58, SURREALO:1, TARSKI:def 1;
then A59: (born u) (+) (born w) in (born x) (+) (born y) by ORDINAL7:94;
then S₁[(born u) (+) (born w)] by A3, A2;
hence ex O being Ordinal st
( O in (born x) (+) (born y) & z in Day O ) by A59, A58; :: thesis: verum

end;

suppose ( z in {x} ++ (L_ y) or z in {x} ++ (R_ y) ) ; :: thesis: ex O being Ordinal st
( O in (born x) (+) (born y) & z in Day O )

then ( ex u, w being Surreal st
( u in {x} & w in L_ y & z = u + w ) or ex u, w being Surreal st
( u in {x} & w in R_ y & z = u + w ) ) by Def8;
then consider u, w being Surreal such that
A60: ( u in {x} & ( w in L_ y or w in R_ y ) & z = u + w ) ;
w in (L_ y) \/ (R_ y) by A60, XBOOLE_0:def 3;
then ( born w in born y & u = x ) by A60, SURREALO:1, TARSKI:def 1;
then A61: (born u) (+) (born w) in (born x) (+) (born y) by ORDINAL7:94;
then S₁[(born u) (+) (born w)] by A3, A2;
hence ex O being Ordinal st
( O in (born x) (+) (born y) & z in Day O ) by A61, A60; :: thesis: verum

end;

end;

end;

then [(((L_ x) ++ {y}) \/ ({x} ++ (L_ y))),(((R_ x) ++ {y}) \/ ({x} ++ (R_ y)))] in Day ((born x) (+) (born y)) by A57, SURREAL0:46;
hence ( x + y is surreal & x + y in Day ((born x) (+) (born y)) ) by Th28; :: thesis: verum

end;

defpred S₂[ Ordinal] means for x, y, z, xz, yz being Surreal st ((born x) (+) (born y)) (+) (born z) c= $1 & (born x) (+) (born z) c= D & (born y) (+) (born z) c= D & xz = x + z & yz = y + z holds
( xz <= yz iff x <= y );
A62: for E being Ordinal st ( for C being Ordinal st C in E holds
S₂[C] ) holds
S₂[E]

proof

let E be Ordinal; :: thesis: ( ( for C being Ordinal st C in E holds
S₂[C] ) implies S₂[E] )
assume A63: for C being Ordinal st C in E holds
S₂[C] ; :: thesis: S₂[E]
let x, y, z, xz, yz be Surreal; :: thesis: ( ((born x) (+) (born y)) (+) (born z) c= E & (born x) (+) (born z) c= D & (born y) (+) (born z) c= D & xz = x + z & yz = y + z implies ( xz <= yz iff x <= y ) )
assume A64: ( ((born x) (+) (born y)) (+) (born z) c= E & (born x) (+) (born z) c= D & (born y) (+) (born z) c= D & xz = x + z & yz = y + z ) ; :: thesis: ( xz <= yz iff x <= y )
A65: xz = [(((L_ x) ++ {z}) \/ ({x} ++ (L_ z))),(((R_ x) ++ {z}) \/ ({x} ++ (R_ z)))] by A64, Th28;
A66: yz = [(((L_ y) ++ {z}) \/ ({y} ++ (L_ z))),(((R_ y) ++ {z}) \/ ({y} ++ (R_ z)))] by A64, Th28;
thus ( xz <= yz implies x <= y ) :: thesis: ( x <= y implies xz <= yz )

proof

assume xz <= yz ; :: thesis: x <= y
then A67: ( L_ xz << {yz} & {xz} << R_ yz ) by SURREAL0:43;
A68: L_ x << {y}

proof

let xL, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not xL in L_ x or not r in {y} or not r <= xL )
assume A69: ( xL in L_ x & r in {y} ) ; :: thesis: not r <= xL
A70: xL in (L_ x) \/ (R_ x) by A69, XBOOLE_0:def 3;
then A71: (born xL) (+) (born z) in (born x) (+) (born z) by SURREALO:1, ORDINAL7:94;
then reconsider xLz = xL + z as Surreal by A2, A64;
(born xL) (+) (born y) in (born x) (+) (born y) by A70, SURREALO:1, ORDINAL7:94;
then A72: ((born xL) (+) (born y)) (+) (born z) in ((born x) (+) (born y)) (+) (born z) by ORDINAL7:94;
A73: (born xL) (+) (born z) c= D by A71, A64, ORDINAL1:def 2;
A74: r = y by A69, TARSKI:def 1;
assume not xL < r ; :: thesis: contradiction
then A75: yz <= xLz by A74, A72, A64, A63, A73;
z in {z} by TARSKI:def 1;
then xLz in (L_ x) ++ {z} by A69, Def8;
then A76: xLz in L_ xz by A65, XBOOLE_0:def 3;
yz in {yz} by TARSKI:def 1;
hence contradiction by A75, A76, A67; :: thesis: verum

end;

{x} << R_ y

proof

let l, yR be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {x} or not yR in R_ y or not yR <= l )
assume A77: ( l in {x} & yR in R_ y ) ; :: thesis: not yR <= l
A78: yR in (L_ y) \/ (R_ y) by A77, XBOOLE_0:def 3;
then A79: (born yR) (+) (born z) in (born y) (+) (born z) by SURREALO:1, ORDINAL7:94;
then reconsider yRz = yR + z as Surreal by A64, A2;
(born x) (+) (born yR) in (born x) (+) (born y) by A78, SURREALO:1, ORDINAL7:94;
then A80: ((born x) (+) (born yR)) (+) (born z) in ((born x) (+) (born y)) (+) (born z) by ORDINAL7:94;
A81: (born yR) (+) (born z) c= D by A79, A64, ORDINAL1:def 2;
A82: l = x by A77, TARSKI:def 1;
assume not l < yR ; :: thesis: contradiction
then A83: yRz <= xz by A82, A80, A63, A64, A81;
z in {z} by TARSKI:def 1;
then yRz in (R_ y) ++ {z} by A77, Def8;
then A84: yRz in R_ yz by A66, XBOOLE_0:def 3;
xz in {xz} by TARSKI:def 1;
hence contradiction by A83, A84, A67; :: thesis: verum

end;

hence x <= y by A68, SURREAL0:43; :: thesis: verum

end;

assume A85: x <= y ; :: thesis: xz <= yz
then A86: ( L_ x << {y} & {x} << R_ y ) by SURREAL0:43;
A87: (L_ x) ++ {z} << {yz}

proof

let L, R be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not L in (L_ x) ++ {z} or not R in {yz} or not R <= L )
assume A88: ( L in (L_ x) ++ {z} & R in {yz} ) ; :: thesis: not R <= L
consider x1, z1 being Surreal such that
A89: ( x1 in L_ x & z1 in {z} & L = x1 + z1 ) by A88, Def8;
A90: ( z1 = z & R = yz ) by A88, A89, TARSKI:def 1;
A91: x1 in (L_ x) \/ (R_ x) by A89, XBOOLE_0:def 3;
then (born x1) (+) (born y) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then A92: ((born x1) (+) (born y)) (+) (born z) in ((born x) (+) (born y)) (+) (born z) by ORDINAL7:94;
y in {y} by TARSKI:def 1;
then A93: x1 < y by A89, A86;
(born x1) (+) (born z) in (born x) (+) (born z) by A91, SURREALO:1, ORDINAL7:94;
then (born x1) (+) (born z) c= D by A64, ORDINAL1:def 2;
hence L < R by A93, A90, A64, A92, A63, A89; :: thesis: verum

end;

A94: {x} ++ (L_ z) << {yz}

proof

let L, R be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not L in {x} ++ (L_ z) or not R in {yz} or not R <= L )
assume A95: ( L in {x} ++ (L_ z) & R in {yz} ) ; :: thesis: not R <= L
consider x1, z1 being Surreal such that
A96: ( x1 in {x} & z1 in L_ z & L = x1 + z1 ) by A95, Def8;
A97: ( x1 = x & R = yz ) by A95, A96, TARSKI:def 1;
assume A98: R <= L ; :: thesis: contradiction
A99: z1 in (L_ z) \/ (R_ z) by A96, XBOOLE_0:def 3;
then A100: ( (born x) (+) (born z1) in (born x) (+) (born z) & (born y) (+) (born z1) in (born y) (+) (born z) ) by SURREALO:1, ORDINAL7:94;
then reconsider xz1 = x + z1, yz1 = y + z1 as Surreal by A2, A64;
A101: ((born x) (+) (born y)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) by A99, SURREALO:1, ORDINAL7:94;
A102: ( (born x) (+) (born z1) c= D & (born y) (+) (born z1) c= D ) by A100, A64, ORDINAL1:def 2;
A103: xz1 <= yz1 by A85, A101, A64, A63, A102;
A104: yz = [(((L_ y) ++ {z}) \/ ({y} ++ (L_ z))),(((R_ y) ++ {z}) \/ ({y} ++ (R_ z)))] by Th28, A64;
A105: L_ yz << {yz} by SURREALO:11;
A106: yz in {yz} by TARSKI:def 1;
y in {y} by TARSKI:def 1;
then yz1 in {y} ++ (L_ z) by A96, Def8;
then yz1 in ((L_ y) ++ {z}) \/ ({y} ++ (L_ z)) by XBOOLE_0:def 3;
hence contradiction by A103, A106, A105, A104, A96, A97, A98, SURREALO:4; :: thesis: verum

end;

A107: {xz} << (R_ y) ++ {z}

proof

let L, R be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not L in {xz} or not R in (R_ y) ++ {z} or not R <= L )
assume A108: ( L in {xz} & R in (R_ y) ++ {z} ) ; :: thesis: not R <= L
consider y1, z1 being Surreal such that
A109: ( y1 in R_ y & z1 in {z} & R = y1 + z1 ) by A108, Def8;
A110: ( z1 = z & L = xz ) by A108, A109, TARSKI:def 1;
A111: y1 in (L_ y) \/ (R_ y) by A109, XBOOLE_0:def 3;
then (born x) (+) (born y1) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then A112: ((born x) (+) (born y1)) (+) (born z) in ((born x) (+) (born y)) (+) (born z) by ORDINAL7:94;
x in {x} by TARSKI:def 1;
then A113: x < y1 by A109, A86;
(born y1) (+) (born z) in (born y) (+) (born z) by A111, SURREALO:1, ORDINAL7:94;
then (born y1) (+) (born z) c= D by A64, ORDINAL1:def 2;
hence L < R by A113, A110, A64, A112, A63, A109; :: thesis: verum

end;

A114: {xz} << {y} ++ (R_ z)

proof

let L, R be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not L in {xz} or not R in {y} ++ (R_ z) or not R <= L )
assume A115: ( L in {xz} & R in {y} ++ (R_ z) ) ; :: thesis: not R <= L
consider y1, z2 being Surreal such that
A116: ( y1 in {y} & z2 in R_ z & R = y1 + z2 ) by A115, Def8;
A117: ( y1 = y & L = xz ) by A115, A116, TARSKI:def 1;
assume A118: R <= L ; :: thesis: contradiction
A119: z2 in (L_ z) \/ (R_ z) by A116, XBOOLE_0:def 3;
then A120: ( (born x) (+) (born z2) in (born x) (+) (born z) & (born y) (+) (born z2) in (born y) (+) (born z) ) by SURREALO:1, ORDINAL7:94;
then reconsider xz2 = x + z2, yz2 = y + z2 as Surreal by A2, A64;
A121: ((born x) (+) (born y)) (+) (born z2) in ((born x) (+) (born y)) (+) (born z) by A119, SURREALO:1, ORDINAL7:94;
( (born x) (+) (born z2) c= D & (born y) (+) (born z2) c= D ) by A120, A64, ORDINAL1:def 2;
then A122: xz2 <= yz2 by A64, A63, A121, A85;
A123: xz = [(((L_ x) ++ {z}) \/ ({x} ++ (L_ z))),(((R_ x) ++ {z}) \/ ({x} ++ (R_ z)))] by Th28, A64;
A124: {xz} << R_ xz by SURREALO:11;
A125: xz in {xz} by TARSKI:def 1;
x in {x} by TARSKI:def 1;
then xz2 in {x} ++ (R_ z) by A116, Def8;
then xz2 in ((R_ x) ++ {z}) \/ ({x} ++ (R_ z)) by XBOOLE_0:def 3;
hence contradiction by A123, A122, A125, A124, A116, A117, A118, SURREALO:4; :: thesis: verum

end;

A126: L_ xz << {yz}

proof

let L, R be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not L in L_ xz or not R in {yz} or not R <= L )
assume A127: ( L in L_ xz & R in {yz} ) ; :: thesis: not R <= L
xz = [(((L_ x) ++ {z}) \/ ({x} ++ (L_ z))),(((R_ x) ++ {z}) \/ ({x} ++ (R_ z)))] by Th28, A64;
then ( L in (L_ x) ++ {z} or L in {x} ++ (L_ z) ) by A127, XBOOLE_0:def 3;
hence not R <= L by A127, A87, A94; :: thesis: verum

end;

{xz} << R_ yz

proof

let L, R be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not L in {xz} or not R in R_ yz or not R <= L )
assume A128: ( L in {xz} & R in R_ yz ) ; :: thesis: not R <= L
yz = [(((L_ y) ++ {z}) \/ ({y} ++ (L_ z))),(((R_ y) ++ {z}) \/ ({y} ++ (R_ z)))] by Th28, A64;
then ( R in (R_ y) ++ {z} or R in {y} ++ (R_ z) ) by A128, XBOOLE_0:def 3;
hence not R <= L by A128, A107, A114; :: thesis: verum

end;

hence xz <= yz by A126, SURREAL0:43; :: thesis: verum

end;

A129: for E being Ordinal holds S₂[E] from ORDINAL1:sch 2(A62);
let x, y, z, xz, yz be Surreal; :: thesis: ( (born x) (+) (born z) c= D & (born y) (+) (born z) c= D & xz = x + z & yz = y + z implies ( xz <= yz iff x <= y ) )
assume A130: ( (born x) (+) (born z) c= D & (born y) (+) (born z) c= D & xz = x + z & yz = y + z ) ; :: thesis: ( xz <= yz iff x <= y )
S₂[((born x) (+) (born y)) (+) (born z)] by A129;
hence ( xz <= yz iff x <= y ) by A130; :: thesis: verum

end;

for E being Ordinal holds S₁[E] from ORDINAL1:sch 2(A1);
hence for D being Ordinal holds
( ( for x, y being Surreal st (born x) (+) (born y) c= D holds
( x + y is surreal & x + y in Day ((born x) (+) (born y)) ) ) & ( for x, y, z, xz, yz being Surreal st (born x) (+) (born z) c= D & (born y) (+) (born z) c= D & xz = x + z & yz = y + z holds
( xz <= yz iff x <= y ) ) ) ; :: thesis: verum