defpred S₁[ Ordinal, Surreal, Surreal] means ( (born $2) (+) (born $3) c= $1 implies $2 * $3 = $3 * $2 );
defpred S₂[ Ordinal, Surreal, Surreal] means ( (born $2) (+) (born $3) c= $1 implies $2 * $3 is Surreal );
defpred S₃[ Ordinal, Surreal, Surreal, Surreal] means for x1y, x2y being Surreal st (born $2) (+) (born $4) c= $1 & (born $3) (+) (born $4) c= $1 & $2 == $3 & x1y = $2 * $4 & x2y = $3 * $4 holds
x1y == x2y;
defpred S₄[ Ordinal, Surreal, Surreal, Surreal, Surreal] means for x1y2, x2y1, x1y1, x2y2 being Surreal st (born $2) (+) (born $4) c= $1 & (born $3) (+) (born $4) c= $1 & (born $2) (+) (born $5) c= $1 & (born $3) (+) (born $5) c= $1 & x1y1 = $2 * $4 & x1y2 = $2 * $5 & x2y1 = $3 * $4 & x2y2 = $3 * $5 & $2 < $3 & $4 < $5 holds
x1y2 + x2y1 < x1y1 + x2y2;
defpred S₅[ Ordinal, Surreal, Surreal, Surreal] means ( $3 < $4 implies ( ( for x being Surreal st x in L_ $2 holds
S₄[$1,x,$2,$3,$4] ) & ( for x being Surreal st x in R_ $2 holds
S₄[$1,$2,x,$3,$4] ) ) );
defpred S₆[ Ordinal] means for x, y being Surreal holds S₁[$1,x,y];
defpred S₇[ Ordinal] means for x, y being Surreal holds S₂[$1,x,y];
defpred S₈[ Ordinal] means for x1, x2, y being Surreal holds S₃[$1,x1,x2,y];
defpred S₉[ Ordinal] means for x1, x2, y1, y2 being Surreal holds S₄[$1,x1,x2,y1,y2];
defpred S₁₀[ Ordinal] means ( S₆[$1] & S₇[$1] & S₈[$1] & S₉[$1] );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁₀[C] ) holds
S₁₀[D]

let D be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in D holds
S₁₀[C] ; :: thesis:
thus A3: for x, y being Surreal holds S₁[D,x,y] :: thesis:

A4: for x, y being Surreal st (born x) (+) (born y) c= D holds
for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
comp (X,x,y,Y) c= comp (Y,y,x,X)

let x, y be Surreal; :: thesis:
assume A5: (born x) (+) (born y) c= D ; :: thesis:
let X, Y be surreal-membered set ; :: thesis:
assume A6: ( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) ) ; :: thesis:
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in comp (X,x,y,Y) ; :: thesis:
then consider x1, y1 being Surreal such that
A7: ( a = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) by Def14;
A8: ( (born x1) (+) (born y1) in (born x1) (+) (born y) & (born x) (+) (born y1) in (born x) (+) (born y) & (born x1) (+) (born y) in (born x) (+) (born y) ) by SURREALO:1, A6, A7, ORDINAL7:94;
then (born x1) (+) (born y1) in (born x) (+) (born y) by ORDINAL1:10;
then A9: ( x1 * y1 = y1 * x1 & x * y1 = y1 * x & x1 * y = y * x1 ) by A8, A2, A5;
reconsider yx1 = y * x1, y1x = y1 * x as Surreal by A8, A2, A5;
(y * x1) +' (y1 * x) = y1x + yx1 by Def11
.= (y1 * x) +' (y * x1) ;
hence a in comp (Y,y,x,X) by A7, Def14, A9; :: thesis:

end;

A10: for x, y being Surreal st (born x) (+) (born y) c= D holds
for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
comp (X,x,y,Y) = comp (Y,y,x,X)

let x, y be Surreal; :: thesis:
assume A11: (born x) (+) (born y) c= D ; :: thesis:
let X, Y be surreal-membered set ; :: thesis:
assume A12: ( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) ) ; :: thesis:
( comp (X,x,y,Y) c= comp (Y,y,x,X) & comp (Y,y,x,X) c= comp (X,x,y,Y) ) by A11, A12, A4;
hence comp (X,x,y,Y) = comp (Y,y,x,X) by XBOOLE_0:def 10; :: thesis:

end;

let x, y be Surreal; :: thesis:
assume A13: (born x) (+) (born y) c= D ; :: thesis:
( L_ x c= (L_ x) \/ (R_ x) & R_ x c= (L_ x) \/ (R_ x) & L_ y c= (L_ y) \/ (R_ y) & R_ y c= (L_ y) \/ (R_ y) ) by XBOOLE_1:7;
then A14: ( comp ((L_ x),x,y,(L_ y)) = comp ((L_ y),y,x,(L_ x)) & comp ((R_ x),x,y,(R_ y)) = comp ((R_ y),y,x,(R_ x)) & comp ((L_ x),x,y,(R_ y)) = comp ((R_ y),y,x,(L_ x)) & comp ((R_ x),x,y,(L_ y)) = comp ((L_ y),y,x,(R_ x)) ) by A10, A13;
x * y = [((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))),((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))))] by Th50
.= y * x by A14, Th50 ;
hence x * y = y * x ; :: thesis:

end;

thus for x, y being Surreal holds S₂[D,x,y] :: thesis:

let x, y be Surreal; :: thesis:
assume A15: (born x) (+) (born y) c= D ; :: thesis:
set CC = ((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))));
A16: for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
comp (X,x,y,Y) is surreal-membered

let X, Y be surreal-membered set ; :: thesis:
assume A17: ( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) ) ; :: thesis:
let z be object ; :: according to SURREAL0:def 16 :: thesis:
assume z in comp (X,x,y,Y) ; :: thesis:
then consider x1, y1 being Surreal such that
A18: ( z = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) by Def14;
A19: ( (born x1) (+) (born y1) in (born x1) (+) (born y) & (born x) (+) (born y1) in (born x) (+) (born y) & (born x1) (+) (born y) in (born x) (+) (born y) ) by A17, SURREALO:1, A18, ORDINAL7:94;
then (born x1) (+) (born y1) in (born x) (+) (born y) by ORDINAL1:10;
then reconsider x1y = x1 * y, xy1 = x * y1, x1y1 = x1 * y1 as Surreal by A19, A15, A2;
thus z is surreal by A18; :: thesis:

end;

A20: ( L_ x c= (L_ x) \/ (R_ x) & R_ x c= (L_ x) \/ (R_ x) & L_ y c= (L_ y) \/ (R_ y) & R_ y c= (L_ y) \/ (R_ y) ) by XBOOLE_1:7;
defpred S₁₁[ object , object ] means ( $1 is Surreal & ( for z being Surreal st z = $1 holds
$2 = born z ) );
A21: for x, y, z being object st S₁₁[x,y] & S₁₁[x,z] holds
y = z

let x, y, z be object ; :: thesis:
assume A22: ( S₁₁[x,y] & S₁₁[x,z] ) ; :: thesis:
reconsider x = x as Surreal by A22;
thus y = born x by A22
.= z by A22 ; :: thesis:

end;

consider OO being set such that
A23: for z being object holds
( z in OO iff ex y being object st
( y in ((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))) & S₁₁[y,z] ) ) from TARSKI_0:sch 1(A21);
for x being set st x in OO holds
x is ordinal

let x be set ; :: thesis:
assume x in OO ; :: thesis:
then consider y being object such that
A24: ( y in ((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))) & S₁₁[y,x] ) by A23;
reconsider y = y as Surreal by A24;
x = born y by A24;
hence x is ordinal ; :: thesis:

end;

then OO is ordinal-membered by ORDINAL6:1;
then reconsider U = union OO as Ordinal ;
A25: for o being object st o in ((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))) holds
ex O being Ordinal st
( O in succ U & o in Day O )

let o be object ; :: thesis:
assume A26: o in ((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))) ; :: thesis:
A27: ( comp ((L_ x),x,y,(L_ y)) is surreal-membered & comp ((R_ x),x,y,(R_ y)) is surreal-membered & comp ((L_ x),x,y,(R_ y)) is surreal-membered & comp ((R_ x),x,y,(L_ y)) is surreal-membered ) by A16, A20;
( o in (comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y))) or o in (comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))) ) by A26, XBOOLE_0:def 3;
then ( o in comp ((L_ x),x,y,(L_ y)) or o in comp ((R_ x),x,y,(R_ y)) or o in comp ((L_ x),x,y,(R_ y)) or o in comp ((R_ x),x,y,(L_ y)) ) by XBOOLE_0:def 3;
then reconsider o = o as Surreal by A27;
S₁₁[o, born o] ;
then born o c= U by A23, A26, ZFMISC_1:74;
then A28: born o in succ U by ORDINAL1:6, ORDINAL1:12;
o in Day (born o) by SURREAL0:def 18;
hence ex O being Ordinal st
( O in succ U & o in Day O ) by A28; :: thesis:

end;

(comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y))) << (comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A29: ( l in (comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y))) & r in (comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))) ) ; :: thesis:

per cases by A29, XBOOLE_0:def 3;

suppose A30: ( l in comp ((L_ x),x,y,(L_ y)) & r in comp ((L_ x),x,y,(R_ y)) ) ; :: thesis:

then consider xL1, yL being Surreal such that
A31: ( l = ((xL1 * y) +' (x * yL)) +' (-' (xL1 * yL)) & xL1 in L_ x & yL in L_ y ) by Def14;
consider xL2, yR being Surreal such that
A32: ( r = ((xL2 * y) +' (x * yR)) +' (-' (xL2 * yR)) & xL2 in L_ x & yR in R_ y ) by Def14, A30;
( xL1 in (L_ x) \/ (R_ x) & xL2 in (L_ x) \/ (R_ x) ) by A31, A32, XBOOLE_0:def 3;
then A33: ( (born xL1) (+) (born y) in (born x) (+) (born y) & (born xL2) (+) (born y) in (born x) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then reconsider xL1y = xL1 * y, xL2y = xL2 * y as Surreal by A15, A2;
set BL = ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y));
A34: ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) in (born x) (+) (born y) by A33, ORDINAL3:12;
A35: ( (born xL1) (+) (born y) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) & (born xL2) (+) (born y) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) ) by XBOOLE_1:7;
A36: ( xL1 == xL2 implies xL1y == xL2y ) by A35, A34, A15, A2;
A37: ( yR in (L_ y) \/ (R_ y) & yL in (L_ y) \/ (R_ y) ) by A31, A32, XBOOLE_0:def 3;
then A38: ( (born xL1) (+) (born yL) in (born xL1) (+) (born y) & (born xL1) (+) (born yR) in (born xL1) (+) (born y) & (born xL2) (+) (born yL) in (born xL2) (+) (born y) & (born xL2) (+) (born yR) in (born xL2) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then ( (born xL1) (+) (born yL) in (born x) (+) (born y) & (born xL1) (+) (born yR) in (born x) (+) (born y) & (born xL2) (+) (born yR) in (born x) (+) (born y) & (born xL2) (+) (born yL) in (born x) (+) (born y) ) by A33, ORDINAL1:10;
then reconsider xL1yR = xL1 * yR, xL2yR = xL2 * yR, xL2yL = xL2 * yL, xL1yL = xL1 * yL as Surreal by A15, A2;
set BY = ((born x) (+) (born yL)) \/ ((born x) (+) (born yR));
A39: ( (born x) (+) (born yL) in (born x) (+) (born y) & (born x) (+) (born yR) in (born x) (+) (born y) ) by A37, SURREALO:1, ORDINAL7:94;
then reconsider xyL = x * yL, xyR = x * yR as Surreal by A15, A2;
A40: ( (born xL1) (+) (born yR) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) & (born xL2) (+) (born yR) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) & (born xL2) (+) (born yL) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) & (born xL1) (+) (born yL) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) ) by A38, A35, ORDINAL1:def 2;
A41: ( xL1 == xL2 implies xL1yR == xL2yR ) by A40, A34, A15, A2;
L_ y << R_ y by SURREAL0:45;
then A42: yL < yR by A31, A32;
( x <= x & y <= y ) ;
then A43: ( L_ x << {x} & {x} << R_ x & x in {x} & L_ y << {y} & {y} << R_ y & y in {y} ) by SURREAL0:43, TARSKI:def 1;
then A44: ( xL1 < x & xL2 < x & yL < y ) by A31, A32;
A45: ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) in (born x) (+) (born y) by A39, ORDINAL3:12;
A46: ( (born x) (+) (born yL) c= ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) & (born x) (+) (born yR) c= ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) ) by XBOOLE_1:7;
set BB = (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR)));
A47: (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) in (born x) (+) (born y) by A34, A45, ORDINAL3:12;
A48: ( ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) ) by XBOOLE_1:7;
then A49: ( (born xL1) (+) (born yL) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born xL1) (+) (born yR) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born x) (+) (born yL) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born x) (+) (born yR) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) ) by A40, A46, XBOOLE_1:1;
A50: ( (born xL1) (+) (born y) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born xL2) (+) (born y) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) ) by A35, A48, XBOOLE_1:1;
A51: ( (born yL) (+) (born xL2) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born yR) (+) (born xL2) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) ) by A40, A48, XBOOLE_1:1;
xL1yR + xyL < xL1yL + xyR by A47, A15, A2, A49, A42, A44;
then xyL < (xL1yL + xyR) - xL1yR by Th42;
then xyL < xL1yL + (xyR - xL1yR) by Th37;
then A52: xyL - xL1yL < xyR - xL1yR by Th41;

suppose A53: xL1 < xL2 ; :: thesis:

xL2yL + xL1y < xL1yL + xL2y by A53, A44, A49, A50, A51, A47, A15, A2;
then xL1y < (xL1yL + xL2y) - xL2yL by Th42;
then xL1y < xL1yL + (xL2y - xL2yL) by Th37;
then xL1y - xL1yL < xL2y - xL2yL by Th41;
then A54: (xL1y + (- xL1yL)) + xyL <= (xL2y - xL2yL) + xyL by Th32;
A55: (xL2y - xL2yL) + xyL = (xyL - xL2yL) + xL2y by Th37;
xL2yR + xyL < xL2yL + xyR by A42, A44, A47, A15, A2, A49, A51;
then xyL < (xL2yL + xyR) - xL2yR by Th42;
then xyL < xL2yL + (xyR - xL2yR) by Th37;
then xyL - xL2yL < xyR - xL2yR by Th41;
then (xyL - xL2yL) + xL2y < (xyR - xL2yR) + xL2y by Th32;
then (xL1y - xL1yL) + xyL < (xyR - xL2yR) + xL2y by SURREALO:4, A54, A55;
then xL1y + ((- xL1yL) + xyL) < (xyR + (- xL2yR)) + xL2y by Th37;
then xL1y + (xyL - xL1yL) < xyR + (xL2y - xL2yR) by Th37;
then (xL1y + xyL) - xL1yL < xyR + (xL2y - xL2yR) by Th37;
then (xL1y + xyL) + (- xL1yL) < (xL2y + xyR) + (- xL2yR) by Th37;
hence l < r by A31, A32; :: thesis:

end;

suppose A56: xL2 < xL1 ; :: thesis:

A57: ( (born y) (+) (born xL1) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born yR) (+) (born xL1) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) ) by A48, A40, XBOOLE_1:1, A35;
( y < yR & xL2 < xL1 ) by A56, A43, A32;
then xL1y + xL2yR < xL2y + xL1yR by A50, A51, A57, A47, A15, A2;
then xL1y < (xL2y + xL1yR) - xL2yR by Th42;
then xL1y < xL1yR + (xL2y - xL2yR) by Th37;
then xL1y - xL1yR < xL2y - xL2yR by Th41;
then (xL1y - xL1yR) + xyR < (xL2y + (- xL2yR)) + xyR by Th32;
then (xL1y - xL1yR) + xyR < (xL2y + xyR) + (- xL2yR) by Th37;
then A58: xL1y + (xyR + (- xL1yR)) < (xL2y + xyR) + (- xL2yR) by Th37;
xL1yR + xyL < xL1yL + xyR by A42, A44, A47, A15, A2, A49;
then xyL < (xL1yL + xyR) - xL1yR by Th42;
then xyL < xL1yL + (xyR - xL1yR) by Th37;
then xyL - xL1yL < xyR - xL1yR by Th41;
then xL1y + (xyL - xL1yL) <= xL1y + (xyR - xL1yR) by Th32;
then xL1y + (xyL - xL1yL) < (xL2y + xyR) - xL2yR by A58, SURREALO:4;
then (xL1y + xyL) + (- xL1yL) < (xL2y + xyR) - xL2yR by Th37;
hence l < r by A31, A32; :: thesis:

end;

suppose A59: xL1 == xL2 ; :: thesis:

then - xL1yR <= - xL2yR by A41, Th10;
then A60: (xL2y + xyR) - xL1yR <= (xL2y + xyR) - xL2yR by Th32;
xL1y + (xyL - xL1yL) < xL2y + (xyR - xL1yR) by A59, A36, A52, Th44;
then xL1y + (xyL - xL1yL) < (xL2y + xyR) - xL1yR by Th37;
then xL1y + (xyL - xL1yL) < (xL2y + xyR) - xL2yR by A60, SURREALO:4;
then (xL1y + xyL) - xL1yL < (xL2y + xyR) - xL2yR by Th37;
hence l < r by A31, A32; :: thesis:

end;

end;

end;

suppose A61: ( l in comp ((R_ x),x,y,(R_ y)) & r in comp ((R_ x),x,y,(L_ y)) ) ; :: thesis:

then consider xR1, yR being Surreal such that
A62: ( l = ((xR1 * y) +' (x * yR)) +' (-' (xR1 * yR)) & xR1 in R_ x & yR in R_ y ) by Def14;
consider xR2, yL being Surreal such that
A63: ( r = ((xR2 * y) +' (x * yL)) +' (-' (xR2 * yL)) & xR2 in R_ x & yL in L_ y ) by Def14, A61;
( xR1 in (L_ x) \/ (R_ x) & xR2 in (L_ x) \/ (R_ x) ) by A62, A63, XBOOLE_0:def 3;
then A64: ( (born xR1) (+) (born y) in (born x) (+) (born y) & (born xR2) (+) (born y) in (born x) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then reconsider xR1y = xR1 * y, xR2y = xR2 * y as Surreal by A15, A2;
set BR = ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y));
A65: ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) in (born x) (+) (born y) by A64, ORDINAL3:12;
A66: ( (born xR1) (+) (born y) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) & (born xR2) (+) (born y) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) ) by XBOOLE_1:7;
A67: ( xR1 == xR2 implies xR1y == xR2y ) by A66, A65, A15, A2;
A68: ( yR in (L_ y) \/ (R_ y) & yL in (L_ y) \/ (R_ y) ) by A62, A63, XBOOLE_0:def 3;
then A69: ( (born xR1) (+) (born yL) in (born xR1) (+) (born y) & (born xR1) (+) (born yR) in (born xR1) (+) (born y) & (born xR2) (+) (born yL) in (born xR2) (+) (born y) & (born xR2) (+) (born yR) in (born xR2) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
( (born xR1) (+) (born yL) in (born x) (+) (born y) & (born xR1) (+) (born yR) in (born x) (+) (born y) & (born xR2) (+) (born yR) in (born x) (+) (born y) & (born xR2) (+) (born yL) in (born x) (+) (born y) ) by A69, A64, ORDINAL1:10;
then reconsider xR1yR = xR1 * yR, xR2yR = xR2 * yR, xR2yL = xR2 * yL, xR1yL = xR1 * yL as Surreal by A15, A2;
set BY = ((born x) (+) (born yL)) \/ ((born x) (+) (born yR));
A70: ( (born x) (+) (born yL) in (born x) (+) (born y) & (born x) (+) (born yR) in (born x) (+) (born y) ) by A68, SURREALO:1, ORDINAL7:94;
then reconsider xyL = x * yL, xyR = x * yR as Surreal by A15, A2;
A71: ( (born xR1) (+) (born yR) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) & (born xR2) (+) (born yR) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) & (born xR2) (+) (born yL) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) & (born xR1) (+) (born yL) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) ) by A69, A66, ORDINAL1:def 2;
A72: ( xR1 == xR2 implies xR1yR == xR2yR ) by A71, A65, A15, A2;
L_ y << R_ y by SURREAL0:45;
then A73: yL < yR by A62, A63;
( x <= x & y <= y ) ;
then A74: ( L_ x << {x} & {x} << R_ x & x in {x} & L_ y << {y} & {y} << R_ y & y in {y} ) by SURREAL0:43, TARSKI:def 1;
then A75: ( x < xR1 & x < xR2 & yL < y ) by A62, A63;
A76: ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) in (born x) (+) (born y) by A70, ORDINAL3:12;
A77: ( (born x) (+) (born yL) c= ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) & (born x) (+) (born yR) c= ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) ) by XBOOLE_1:7;
set BB = (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR)));
A78: (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) in (born x) (+) (born y) by A65, A76, ORDINAL3:12;
A79: ( ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) ) by XBOOLE_1:7;
then A80: ( (born xR1) (+) (born yL) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born xR1) (+) (born yR) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born x) (+) (born yL) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born x) (+) (born yR) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) ) by A71, A77, XBOOLE_1:1;
A81: ( (born xR1) (+) (born y) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born xR2) (+) (born y) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) ) by A66, A79, XBOOLE_1:1;
A82: ( (born xR2) (+) (born yL) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born xR2) (+) (born yR) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) ) by A71, A79, XBOOLE_1:1;

suppose A83: xR1 < xR2 ; :: thesis:

( yL < y & xR1 < xR2 ) by A83, A74, A63;
then xR2yL + xR1y < xR1yL + xR2y by A80, A81, A82, A78, A15, A2;
then xR1y < (xR1yL + xR2y) - xR2yL by Th42;
then xR1y < xR1yL + (xR2y - xR2yL) by Th37;
then xR1y - xR1yL < xR2y - xR2yL by Th41;
then (xR1y - xR1yL) + xyL < (xR2y - xR2yL) + xyL by Th32;
then ((- xR1yL) + xR1y) + xyL < (- xR2yL) + (xR2y + xyL) by Th37;
then A84: (xR1y + xyL) - xR1yL < (xR2y + xyL) - xR2yL by Th37;
xyR + xR1yL < xyL + xR1yR by A73, A75, A80, A78, A15, A2;
then (xyR + xR1yL) - xR1yR < xyL by Th41;
then xR1yL + (xyR - xR1yR) < xyL by Th37;
then xyR + (- xR1yR) < xyL - xR1yL by Th42;
then xR1y + (xyR + (- xR1yR)) < xR1y + (xyL + (- xR1yL)) by Th32;
then (xR1y + xyR) + (- xR1yR) < xR1y + (xyL + (- xR1yL)) by Th37;
then (xR1y + xyR) + (- xR1yR) <= (xR1y + xyL) + (- xR1yL) by Th37;
hence not r <= l by A62, A63, A84, SURREALO:4; :: thesis:

end;

suppose A85: xR2 < xR1 ; :: thesis:

( y < yR & xR2 < xR1 ) by A85, A74, A62;
then xR1y + xR2yR < xR2y + xR1yR by A80, A81, A82, A78, A15, A2;
then (xR2yR + xR1y) - xR1yR < xR2y by Th41;
then xR2yR + (xR1y - xR1yR) < xR2y by Th37;
then xR1y + (- xR1yR) < xR2y - xR2yR by Th42;
then (xR1y + (- xR1yR)) + xyR < (xR2y + (- xR2yR)) + xyR by Th32;
then A86: (xR1y + xyR) + (- xR1yR) < (xR2y + (- xR2yR)) + xyR by Th37;
xyR + xR2yL < xyL + xR2yR by A73, A75, A78, A15, A2, A80, A82;
then xyR < (xR2yR + xyL) - xR2yL by Th42;
then xyR < xR2yR + (xyL - xR2yL) by Th37;
then xyR - xR2yR < xyL - xR2yL by Th41;
then xR2y + ((- xR2yR) + xyR) < xR2y + (xyL + (- xR2yL)) by Th32;
then (xR2y + (- xR2yR)) + xyR < xR2y + (xyL + (- xR2yL)) by Th37;
then (xR2y + (- xR2yR)) + xyR <= (xR2y + xyL) + (- xR2yL) by Th37;
hence not r <= l by A62, A63, A86, SURREALO:4; :: thesis:

end;

suppose A87: xR1 == xR2 ; :: thesis:

then - xR1yR <= - xR2yR by A72, Th10;
then A88: (xR1y + xyR) + (- xR1yR) <= (xR1y + xyR) + (- xR2yR) by Th32;
xyR + xR2yL < xyL + xR2yR by A75, A73, A80, A82, A78, A15, A2;
then (xR2yL + xyR) - xR2yR < xyL by Th41;
then xR2yL + (xyR - xR2yR) < xyL by Th37;
then xyR - xR2yR < xyL - xR2yL by Th42;
then xR1y + (xyR - xR2yR) < xR2y + (xyL - xR2yL) by A87, A67, Th44;
then xR1y + (xyR - xR2yR) < (xR2y + xyL) - xR2yL by Th37;
then (xR1y + xyR) + (- xR2yR) < (xR2y + xyL) + (- xR2yL) by Th37;
hence l < r by A88, SURREALO:4, A62, A63; :: thesis:

end;

end;

end;

suppose A89: ( l in comp ((L_ x),x,y,(L_ y)) & r in comp ((R_ x),x,y,(L_ y)) ) ; :: thesis:

then consider xL, yL1 being Surreal such that
A90: ( l = ((xL * y) +' (x * yL1)) +' (-' (xL * yL1)) & xL in L_ x & yL1 in L_ y ) by Def14;
consider xR, yL2 being Surreal such that
A91: ( r = ((xR * y) +' (x * yL2)) +' (-' (xR * yL2)) & xR in R_ x & yL2 in L_ y ) by Def14, A89;
( yL1 in (L_ y) \/ (R_ y) & yL2 in (L_ y) \/ (R_ y) ) by A90, A91, XBOOLE_0:def 3;
then A92: ( (born yL1) (+) (born x) in (born x) (+) (born y) & (born yL2) (+) (born x) in (born x) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then reconsider yL1x = yL1 * x, yL2x = yL2 * x as Surreal by A15, A2;
set BL = ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x));
A93: ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) in (born x) (+) (born y) by A92, ORDINAL3:12;
A94: ( (born yL1) (+) (born x) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) & (born yL2) (+) (born x) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) ) by XBOOLE_1:7;
A95: ( yL1 == yL2 implies yL1x == yL2x ) by A94, A93, A15, A2;
A96: ( xR in (L_ x) \/ (R_ x) & xL in (L_ x) \/ (R_ x) ) by A90, A91, XBOOLE_0:def 3;
A97: ( (born yL1) (+) (born xL) in (born yL1) (+) (born x) & (born yL1) (+) (born xR) in (born yL1) (+) (born x) & (born yL2) (+) (born xL) in (born yL2) (+) (born x) & (born yL2) (+) (born xR) in (born yL2) (+) (born x) ) by A96, SURREALO:1, ORDINAL7:94;
then ( (born yL1) (+) (born xL) in (born x) (+) (born y) & (born yL1) (+) (born xR) in (born x) (+) (born y) & (born yL2) (+) (born xR) in (born x) (+) (born y) & (born yL2) (+) (born xL) in (born x) (+) (born y) ) by A92, ORDINAL1:10;
then reconsider yL1xR = yL1 * xR, yL2xR = yL2 * xR, yL2xL = yL2 * xL, yL1xL = yL1 * xL as Surreal by A15, A2;
set BY = ((born y) (+) (born xL)) \/ ((born y) (+) (born xR));
A98: ( (born y) (+) (born xL) in (born x) (+) (born y) & (born y) (+) (born xR) in (born x) (+) (born y) ) by A96, SURREALO:1, ORDINAL7:94;
then reconsider yxL = y * xL, yxR = y * xR as Surreal by A15, A2;
A99: ( (born yL1) (+) (born xR) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) & (born yL2) (+) (born xR) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) & (born yL2) (+) (born xL) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) & (born yL1) (+) (born xL) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) ) by A97, A94, ORDINAL1:def 2;
A100: ( yL1 == yL2 implies yL1xR == yL2xR ) by A99, A93, A15, A2;
L_ x << R_ x by SURREAL0:45;
then A101: xL < xR by A90, A91;
( x <= x & y <= y ) ;
then A102: ( L_ x << {x} & {x} << R_ x & x in {x} & L_ y << {y} & {y} << R_ y & y in {y} ) by SURREAL0:43, TARSKI:def 1;
then A103: ( yL1 < y & yL2 < y & xL < x ) by A90, A91;
A104: ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) in (born x) (+) (born y) by A98, ORDINAL3:12;
A105: ( (born y) (+) (born xL) c= ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) & (born y) (+) (born xR) c= ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) ) by XBOOLE_1:7;
set BB = (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR)));
A106: (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) in (born x) (+) (born y) by A93, A104, ORDINAL3:12;
A107: ( ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) ) by XBOOLE_1:7;
then A108: ( (born yL1) (+) (born xL) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born yL1) (+) (born xR) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born y) (+) (born xL) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born y) (+) (born xR) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) ) by A99, A105, XBOOLE_1:1;
A109: ( (born yL1) (+) (born x) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born yL2) (+) (born x) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) ) by A94, A107, XBOOLE_1:1;
A110: ( (born xL) (+) (born yL2) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born xR) (+) (born yL2) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) ) by A99, A107, XBOOLE_1:1;
yL1xR + yxL < yL1xL + yxR by A106, A15, A2, A108, A101, A103;
then yxL < (yL1xL + yxR) - yL1xR by Th42;
then yxL < yL1xL + (yxR - yL1xR) by Th37;
then A111: yxL - yL1xL < yxR - yL1xR by Th41;
A112: ( xL * yL2 = yL2xL & x * yL2 = yL2x ) by A2, A106, A15, A109, A110;
A113: ( xL * yL1 = yL1xL & x * yL1 = yL1x ) by A2, A106, A15, A108, A109;
A114: ( xR * yL2 = yL2xR & xR * yL1 = yL1xR ) by A2, A106, A15, A108, A110;
A115: l = (yxL + yL1x) + (- yL1xL) by A90, A2, A106, A15, A108, A113
.= (yL1x + yxL) + (- yL1xL) ;
A116: r = (yxR + yL2x) + (- yL2xR) by A91, A2, A106, A15, A108, A112, A114
.= (yL2x + yxR) + (- yL2xR) ;

suppose A117: yL1 < yL2 ; :: thesis:

yL2xL + yL1x < yL1xL + yL2x by A117, A103, A108, A109, A110, A106, A15, A2;
then yL1x < (yL1xL + yL2x) - yL2xL by Th42;
then yL1x < yL1xL + (yL2x - yL2xL) by Th37;
then yL1x - yL1xL < yL2x - yL2xL by Th41;
then A118: (yL1x + (- yL1xL)) + yxL <= (yL2x - yL2xL) + yxL by Th32;
A119: (yL2x - yL2xL) + yxL = (yxL - yL2xL) + yL2x by Th37;
yL2xR + yxL < yL2xL + yxR by A101, A103, A106, A15, A2, A108, A110;
then yxL < (yL2xL + yxR) - yL2xR by Th42;
then yxL < yL2xL + (yxR + (- yL2xR)) by Th37;
then yxL - yL2xL < yxR + (- yL2xR) by Th41;
then (yxL - yL2xL) + yL2x < (yxR + (- yL2xR)) + yL2x by Th32;
then (yL1x - yL1xL) + yxL < (yxR + (- yL2xR)) + yL2x by SURREALO:4, A118, A119;
then yL1x + ((- yL1xL) + yxL) < (yxR - yL2xR) + yL2x by Th37;
then yL1x + (yxL - yL1xL) < yxR + (yL2x - yL2xR) by Th37;
then (yL1x + yxL) - yL1xL < yxR + (yL2x - yL2xR) by Th37;
hence l < r by A115, A116, Th37; :: thesis:

end;

suppose A120: yL2 < yL1 ; :: thesis:

A121: ( (born x) (+) (born yL1) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born xR) (+) (born yL1) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) ) by A99, XBOOLE_1:1, A94, A107;
( x < xR & yL2 < yL1 ) by A120, A102, A91;
then yL1x + yL2xR < yL2x + yL1xR by A109, A110, A121, A106, A15, A2;
then yL1x < (yL2x + yL1xR) - yL2xR by Th42;
then yL1x < yL1xR + (yL2x - yL2xR) by Th37;
then yL1x - yL1xR < yL2x - yL2xR by Th41;
then (yL1x - yL1xR) + yxR < (yL2x - yL2xR) + yxR by Th32;
then (yL1x - yL1xR) + yxR < (yL2x + yxR) - yL2xR by Th37;
then A122: yL1x + (yxR + (- yL1xR)) < (yL2x + yxR) + (- yL2xR) by Th37;
yL1xR + yxL < yL1xL + yxR by A101, A103, A106, A15, A2, A108;
then yxL < (yL1xL + yxR) - yL1xR by Th42;
then yxL < yL1xL + (yxR - yL1xR) by Th37;
then yxL - yL1xL < yxR - yL1xR by Th41;
then yL1x + (yxL + (- yL1xL)) <= yL1x + (yxR - yL1xR) by Th32;
then yL1x + (yxL + (- yL1xL)) < (yL2x + yxR) + (- yL2xR) by A122, SURREALO:4;
hence l < r by A115, A116, Th37; :: thesis:

end;

suppose A123: yL1 == yL2 ; :: thesis:

then - yL1xR <= - yL2xR by Th10, A100;
then A124: (yL2x + yxR) + (- yL1xR) <= (yL2x + yxR) + (- yL2xR) by Th32;
yL1x + (yxL + (- yL1xL)) < yL2x + (yxR + (- yL1xR)) by A123, A95, A111, Th44;
then yL1x + (yxL + (- yL1xL)) < (yL2x + yxR) + (- yL1xR) by Th37;
then yL1x + (yxL + (- yL1xL)) < (yL2x + yxR) + (- yL2xR) by A124, SURREALO:4;
hence l < r by Th37, A115, A116; :: thesis:

end;

end;

end;

suppose A125: ( l in comp ((R_ x),x,y,(R_ y)) & r in comp ((L_ x),x,y,(R_ y)) ) ; :: thesis:

then consider xR, yR1 being Surreal such that
A126: ( l = ((xR * y) +' (x * yR1)) +' (-' (xR * yR1)) & xR in R_ x & yR1 in R_ y ) by Def14;
consider xL, yR2 being Surreal such that
A127: ( r = ((xL * y) +' (x * yR2)) +' (-' (xL * yR2)) & xL in L_ x & yR2 in R_ y ) by Def14, A125;
( yR1 in (L_ y) \/ (R_ y) & yR2 in (L_ y) \/ (R_ y) ) by A126, A127, XBOOLE_0:def 3;
then A128: ( (born yR1) (+) (born x) in (born y) (+) (born x) & (born yR2) (+) (born x) in (born y) (+) (born x) ) by SURREALO:1, ORDINAL7:94;
then reconsider yR1x = yR1 * x, yR2x = yR2 * x as Surreal by A15, A2;
set BR = ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x));
A129: ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) in (born x) (+) (born y) by A128, ORDINAL3:12;
A130: ( (born yR1) (+) (born x) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) & (born yR2) (+) (born x) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) ) by XBOOLE_1:7;
A131: ( yR1 == yR2 implies yR1x == yR2x ) by A130, A129, A15, A2;
A132: ( xR in (L_ x) \/ (R_ x) & xL in (L_ x) \/ (R_ x) ) by A126, A127, XBOOLE_0:def 3;
A133: ( (born yR1) (+) (born xL) in (born yR1) (+) (born x) & (born yR1) (+) (born xR) in (born yR1) (+) (born x) & (born yR2) (+) (born xL) in (born yR2) (+) (born x) & (born yR2) (+) (born xR) in (born yR2) (+) (born x) ) by A132, SURREALO:1, ORDINAL7:94;
( (born yR1) (+) (born xL) in (born x) (+) (born y) & (born yR1) (+) (born xR) in (born x) (+) (born y) & (born yR2) (+) (born xR) in (born x) (+) (born y) & (born yR2) (+) (born xL) in (born x) (+) (born y) ) by A128, ORDINAL1:10, A133;
then reconsider yR1xR = yR1 * xR, yR2xR = yR2 * xR, yR2xL = yR2 * xL, yR1xL = yR1 * xL as Surreal by A15, A2;
set BY = ((born y) (+) (born xL)) \/ ((born y) (+) (born xR));
A134: ( (born y) (+) (born xL) in (born x) (+) (born y) & (born y) (+) (born xR) in (born x) (+) (born y) ) by A132, SURREALO:1, ORDINAL7:94;
then reconsider yxL = y * xL, yxR = y * xR as Surreal by A15, A2;
A135: ( (born yR1) (+) (born xR) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) & (born yR2) (+) (born xR) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) & (born yR2) (+) (born xL) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) & (born yR1) (+) (born xL) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) ) by A133, A130, ORDINAL1:def 2;
A136: ( yR1 == yR2 implies yR1xR == yR2xR ) by A135, A129, A15, A2;
L_ x << R_ x by SURREAL0:45;
then A137: xL < xR by A126, A127;
( x <= x & y <= y ) ;
then A138: ( L_ x << {x} & {x} << R_ x & x in {x} & L_ y << {y} & {y} << R_ y & y in {y} ) by SURREAL0:43, TARSKI:def 1;
then A139: ( y < yR1 & y < yR2 & xL < x ) by A126, A127;
A140: ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) in (born x) (+) (born y) by A134, ORDINAL3:12;
A141: ( (born y) (+) (born xL) c= ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) & (born y) (+) (born xR) c= ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) ) by XBOOLE_1:7;
set BB = (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR)));
A142: (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) in (born x) (+) (born y) by A129, A140, ORDINAL3:12;
A143: ( ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) ) by XBOOLE_1:7;
then A144: ( (born yR1) (+) (born xL) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born yR1) (+) (born xR) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born y) (+) (born xL) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born y) (+) (born xR) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) ) by A135, A141, XBOOLE_1:1;
A145: ( (born yR1) (+) (born x) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born yR2) (+) (born x) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) ) by A130, A143, XBOOLE_1:1;
A146: ( (born yR2) (+) (born xL) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born yR2) (+) (born xR) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) ) by A135, A143, XBOOLE_1:1;
A147: ( xR * y = yxR & xL * y = yxL ) by A2, A142, A15, A144;
A148: ( xL * yR2 = yR2xL & x * yR2 = yR2x ) by A2, A142, A15, A145, A146;
A149: ( xR * yR2 = yR2xR & xR * yR1 = yR1xR ) by A2, A142, A15, A144, A146;
A150: l = (yxR + yR1x) + (- yR1xR) by A126, A147, A2, A142, A15, A145, A149
.= (yR1x + yxR) + (- yR1xR) ;
A151: r = (yxL + yR2x) + (- yR2xL) by A127, A2, A142, A15, A144, A148
.= (yR2x + yxL) + (- yR2xL) ;

suppose A152: yR1 < yR2 ; :: thesis:

yR2xL + yR1x < yR1xL + yR2x by A152, A139, A144, A145, A146, A142, A15, A2;
then yR1x < (yR1xL + yR2x) - yR2xL by Th42;
then yR1x < yR1xL + (yR2x - yR2xL) by Th37;
then yR1x - yR1xL < yR2x - yR2xL by Th41;
then (yR1x - yR1xL) + yxL < (yR2x - yR2xL) + yxL by Th32;
then ((- yR1xL) + yR1x) + yxL < (- yR2xL) + (yR2x + yxL) by Th37;
then A153: (yR1x + yxL) + (- yR1xL) < (yR2x + yxL) - yR2xL by Th37;
yxR + yR1xL < yxL + yR1xR by A137, A139, A144, A142, A15, A2;
then (yxR + yR1xL) - yR1xR < yxL by Th41;
then yR1xL + (yxR - yR1xR) < yxL by Th37;
then yxR + (- yR1xR) < yxL - yR1xL by Th42;
then yR1x + (yxR - yR1xR) < yR1x + (yxL - yR1xL) by Th32;
then (yR1x + yxR) - yR1xR < yR1x + (yxL - yR1xL) by Th37;
then (yR1x + yxR) - yR1xR <= (yR1x + yxL) - yR1xL by Th37;
hence not r <= l by A151, A150, A153, SURREALO:4; :: thesis:

end;

suppose A154: yR2 < yR1 ; :: thesis:

( x < xR & yR2 < yR1 ) by A154, A138, A126;
then yR1x + yR2xR < yR2x + yR1xR by A144, A145, A146, A142, A15, A2;
then (yR1x + yR2xR) - yR1xR < yR2x by Th41;
then yR2xR + (yR1x - yR1xR) < yR2x by Th37;
then yR1x - yR1xR < yR2x - yR2xR by Th42;
then (yR1x - yR1xR) + yxR < (yR2x - yR2xR) + yxR by Th32;
then A155: (yR1x + yxR) + (- yR1xR) < (yR2x - yR2xR) + yxR by Th37;
yxR + yR2xL < yxL + yR2xR by A137, A139, A142, A15, A2, A144, A146;
then yxR < (yR2xR + yxL) - yR2xL by Th42;
then yxR < yR2xR + (yxL - yR2xL) by Th37;
then yxR - yR2xR < yxL - yR2xL by Th41;
then yR2x + ((- yR2xR) + yxR) < yR2x + (yxL - yR2xL) by Th32;
then (yR2x + (- yR2xR)) + yxR < yR2x + (yxL - yR2xL) by Th37;
then (yR2x - yR2xR) + yxR <= (yR2x + yxL) - yR2xL by Th37;
hence not r <= l by A151, A150, A155, SURREALO:4; :: thesis:

end;

suppose A156: yR1 == yR2 ; :: thesis:

then - yR1xR <= - yR2xR by A136, Th10;
then A157: (yR1x + yxR) - yR1xR <= (yR1x + yxR) - yR2xR by Th32;
yxR + yR2xL < yxL + yR2xR by A139, A137, A144, A146, A142, A15, A2;
then (yR2xL + yxR) - yR2xR < yxL by Th41;
then yR2xL + (yxR - yR2xR) < yxL by Th37;
then yxR - yR2xR < yxL - yR2xL by Th42;
then yR1x + (yxR - yR2xR) < yR2x + (yxL - yR2xL) by A156, A131, Th44;
then yR1x + (yxR - yR2xR) < (yR2x + yxL) - yR2xL by Th37;
then (yR1x + yxR) - yR2xR < (yR2x + yxL) - yR2xL by Th37;
hence l < r by A151, A150, A157, SURREALO:4; :: thesis:

end;

end;

end;

end;

end;

then [((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))),((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))))] in Day (succ U) by A25, SURREAL0:46;
hence x * y is Surreal by Th50; :: thesis:

end;

defpred S₁₁[ Ordinal] means for x1, x2, y being Surreal st ((born x1) (+) (born x2)) (+) (born y) c= $1 holds
( S₃[D,x1,x2,y] & S₅[D,x1,x2,y] );
A158: for E being Ordinal st ( for C being Ordinal st C in E holds
S₁₁[C] ) holds
S₁₁[E]

let E be Ordinal; :: thesis:
assume A159: for C being Ordinal st C in E holds
S₁₁[C] ; :: thesis:
A160: for x1, x2, y, x1y, x2y being Surreal st ((born x1) (+) (born x2)) (+) (born y) c= E & (born x1) (+) (born y) c= D & (born x2) (+) (born y) c= D & x1 == x2 & x1y = x1 * y & x2y = x2 * y holds
( L_ x1y << {x2y} & {x2y} << R_ x1y )

let x1, x2, y, x1y, x2y be Surreal; :: thesis:
assume that
A161: ((born x1) (+) (born x2)) (+) (born y) c= E and
A162: ( (born x1) (+) (born y) c= D & (born x2) (+) (born y) c= D ) and
A163: ( x1 == x2 & x1y = x1 * y & x2y = x2 * y ) ; :: thesis:
A164: x1y = [((comp ((L_ x1),x1,y,(L_ y))) \/ (comp ((R_ x1),x1,y,(R_ y)))),((comp ((L_ x1),x1,y,(R_ y))) \/ (comp ((R_ x1),x1,y,(L_ y))))] by A163, Th50;
A165: ( L_ y << {y} & {y} << R_ y & y in {y} ) by SURREALO:11, TARSKI:def 1;
thus L_ x1y << {x2y} :: thesis:

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A166: ( l in L_ x1y & r in {x2y} ) ; :: thesis:

per cases by A164, A166, XBOOLE_0:def 3;

suppose l in comp ((R_ x1),x1,y,(R_ y)) ; :: thesis:

then consider x3, y3 being Surreal such that
A167: ( l = ((x3 * y) +' (x1 * y3)) +' (-' (x3 * y3)) & x3 in R_ x1 & y3 in R_ y ) by Def14;
A168: ( {x1} << R_ x1 & x1 in {x1} ) by SURREALO:11, TARSKI:def 1;
A169: y3 in (L_ y) \/ (R_ y) by A167, XBOOLE_0:def 3;
then A170: ( (born x1) (+) (born y3) in (born x1) (+) (born y) & (born x2) (+) (born y3) in (born x2) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then reconsider x1y3 = x1 * y3, x2y3 = x2 * y3 as Surreal by A2, A162;
set BL = ((born x1) (+) (born y3)) \/ ((born x2) (+) (born y3));
x3 in (L_ x1) \/ (R_ x1) by A167, XBOOLE_0:def 3;
then A171: ( (born x3) (+) (born y3) in (born x1) (+) (born y3) & (born x3) (+) (born y) in (born x1) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then A172: ( (born x3) (+) (born y3) in D & (born x3) (+) (born y) in D ) by A170, A162, ORDINAL1:10;
then reconsider x3y3 = x3 * y3, x3y = x3 * y as Surreal by A2;
A173: ((born x1) (+) (born x2)) (+) (born y3) in ((born x1) (+) (born x2)) (+) (born y) by A169, SURREALO:1, ORDINAL7:94;
( (born x1) (+) (born y3) c= D & (born x2) (+) (born y3) c= D ) by A170, A162, ORDINAL1:def 2;
then A174: x1y3 == x2y3 by A173, A163, A161, A159;
((born y) (+) (born x3)) (+) (born x2) in ((born y) (+) (born x1)) (+) (born x2) by A171, ORDINAL7:94;
then A175: ((born y) (+) (born x3)) (+) (born x2) in (born y) (+) ((born x1) (+) (born x2)) by ORDINAL7:68;
A176: ((born y) (+) (born x3)) (+) (born x2) = ((born y) (+) (born x2)) (+) (born x3) by ORDINAL7:68;
A177: (born x2) (+) (born y3) c= D by A170, A162, ORDINAL1:def 2;
A178: y3 * x2 = x2y3 by A3, A170, A162, ORDINAL1:def 2;
A179: ( (born x3) (+) (born y) c= D & (born x2) (+) (born y) c= D ) by A171, A162, ORDINAL1:def 2;
A180: ( y * x3 = x3y & y * x2 = x2y ) by A162, A163, A3, A171, A2;
A181: (born x3) (+) (born y3) c= D by A171, A170, A162, ORDINAL1:10, ORDINAL1:def 2;
A182: y3 * x3 = x3y3 by A172, A2;
( y < y3 & x2 < x3 ) by A168, A167, A163, SURREALO:4, A165;
then x2y3 + x3y < x3y3 + x2y by A167, A176, A175, A161, A159, A177, A178, A179, A180, A181, A182;
then A183: (x2y3 + x3y) - x3y3 < x2y by Th41;
x1y3 + (x3y + (- x3y3)) <= x2y3 + (x3y - x3y3) by A174, Th32;
then (x1y3 + x3y) - x3y3 <= x2y3 + (x3y - x3y3) by Th37;
then (x1y3 + x3y) - x3y3 <= (x2y3 + x3y) - x3y3 by Th37;
then A184: (x1y3 + x3y) - x3y3 < x2y by A183, SURREALO:4;
l = (x3y + x1y3) - x3y3 by A167;
hence not r <= l by A166, A184, TARSKI:def 1; :: thesis:

end;

suppose l in comp ((L_ x1),x1,y,(L_ y)) ; :: thesis:

then consider x3, y3 being Surreal such that
A185: ( l = ((x3 * y) +' (x1 * y3)) +' (-' (x3 * y3)) & x3 in L_ x1 & y3 in L_ y ) by Def14;
A186: ( L_ x1 << {x1} & x1 in {x1} ) by SURREALO:11, TARSKI:def 1;
A187: y3 in (L_ y) \/ (R_ y) by A185, XBOOLE_0:def 3;
then A188: ( (born x1) (+) (born y3) in (born x1) (+) (born y) & (born x2) (+) (born y3) in (born x2) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then reconsider x1y3 = x1 * y3, x2y3 = x2 * y3 as Surreal by A2, A162;
set BL = ((born x1) (+) (born y3)) \/ ((born x2) (+) (born y3));
x3 in (L_ x1) \/ (R_ x1) by A185, XBOOLE_0:def 3;
then A189: ( (born x3) (+) (born y3) in (born x1) (+) (born y3) & (born x3) (+) (born y) in (born x1) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then A190: ( (born x3) (+) (born y3) in D & (born x3) (+) (born y) in D ) by A188, A162, ORDINAL1:10;
then reconsider x3y3 = x3 * y3, x3y = x3 * y as Surreal by A2;
A191: ((born x1) (+) (born x2)) (+) (born y3) in ((born x1) (+) (born x2)) (+) (born y) by A187, SURREALO:1, ORDINAL7:94;
( (born x1) (+) (born y3) c= D & (born x2) (+) (born y3) c= D ) by A188, A162, ORDINAL1:def 2;
then A192: x1y3 == x2y3 by A191, A161, A159, A163;
((born y) (+) (born x3)) (+) (born x2) in ((born y) (+) (born x1)) (+) (born x2) by A189, ORDINAL7:94;
then A193: ((born y) (+) (born x3)) (+) (born x2) in (born y) (+) ((born x1) (+) (born x2)) by ORDINAL7:68;
A194: (born x2) (+) (born y3) c= D by A188, A162, ORDINAL1:def 2;
A195: y3 * x2 = x2y3 by A3, A188, A162, ORDINAL1:def 2;
A196: ( (born x3) (+) (born y) c= D & (born x2) (+) (born y) c= D ) by A189, A162, ORDINAL1:def 2;
A197: ( y * x3 = x3y & y * x2 = x2y ) by A163, A3, A162, A189, ORDINAL1:def 2;
A198: (born x3) (+) (born y3) c= D by A188, A162, ORDINAL1:10, A189, ORDINAL1:def 2;
A199: y3 * x3 = x3y3 by A190, A2;
A200: ( y3 < y & x3 < x2 ) by A186, A185, A163, SURREALO:4, A165;
x2y3 + x3y < x3y3 + x2y by A185, A200, A194, A195, A196, A197, A198, A199, A193, A161, A159;
then A201: (x2y3 + x3y) - x3y3 < x2y by Th41;
x1y3 + (x3y + (- x3y3)) <= x2y3 + (x3y + (- x3y3)) by A192, Th32;
then (x1y3 + x3y) + (- x3y3) <= x2y3 + (x3y + (- x3y3)) by Th37;
then (x1y3 + x3y) + (- x3y3) <= (x2y3 + x3y) + (- x3y3) by Th37;
then A202: (x1y3 + x3y) + (- x3y3) < x2y by A201, SURREALO:4;
l = (x3y + x1y3) + (- x3y3) by A185;
hence not r <= l by A166, A202, TARSKI:def 1; :: thesis:

end;

end;

end;

thus {x2y} << R_ x1y :: thesis:

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A203: ( l in {x2y} & r in R_ x1y ) ; :: thesis:

per cases by XBOOLE_0:def 3, A164, A203;

suppose r in comp ((L_ x1),x1,y,(R_ y)) ; :: thesis:

then consider x3, y3 being Surreal such that
A204: ( r = ((x3 * y) +' (x1 * y3)) +' (-' (x3 * y3)) & x3 in L_ x1 & y3 in R_ y ) by Def14;
A205: ( L_ x1 << {x1} & x1 in {x1} ) by SURREALO:11, TARSKI:def 1;
A206: y3 in (L_ y) \/ (R_ y) by A204, XBOOLE_0:def 3;
then A207: ( (born x1) (+) (born y3) in (born x1) (+) (born y) & (born x2) (+) (born y3) in (born x2) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then reconsider x1y3 = x1 * y3, x2y3 = x2 * y3 as Surreal by A162, A2;
set BL = ((born x1) (+) (born y3)) \/ ((born x2) (+) (born y3));
x3 in (L_ x1) \/ (R_ x1) by A204, XBOOLE_0:def 3;
then A208: ( (born x3) (+) (born y3) in (born x1) (+) (born y3) & (born x3) (+) (born y) in (born x1) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then A209: ( (born x3) (+) (born y3) in D & (born x3) (+) (born y) in D ) by A207, A162, ORDINAL1:10;
then reconsider x3y3 = x3 * y3, x3y = x3 * y as Surreal by A2;
A210: ((born x1) (+) (born x2)) (+) (born y3) in ((born x1) (+) (born x2)) (+) (born y) by A206, SURREALO:1, ORDINAL7:94;
( (born x1) (+) (born y3) c= D & (born x2) (+) (born y3) c= D ) by A207, A162, ORDINAL1:def 2;
then A211: x1y3 == x2y3 by A210, A161, A159, A163;
((born y) (+) (born x3)) (+) (born x2) in ((born y) (+) (born x1)) (+) (born x2) by A208, ORDINAL7:94;
then A212: ((born y) (+) (born x3)) (+) (born x2) in (born y) (+) ((born x1) (+) (born x2)) by ORDINAL7:68;
A213: (born x2) (+) (born y3) c= D by A207, A162, ORDINAL1:def 2;
A214: y3 * x2 = x2y3 by A3, A207, A162, ORDINAL1:def 2;
A215: ( (born x3) (+) (born y) c= D & (born x2) (+) (born y) c= D ) by A208, A162, ORDINAL1:def 2;
A216: ( y * x3 = x3y & y * x2 = x2y ) by A208, A162, ORDINAL1:def 2, A163, A3;
A217: (born x3) (+) (born y3) c= D by A207, A162, ORDINAL1:10, A208, ORDINAL1:def 2;
A218: y3 * x3 = x3y3 by A209, A2;
A219: ( y < y3 & x3 < x2 ) by A205, A204, A163, SURREALO:4, A165;
x3y3 + x2y < x2y3 + x3y by A204, A212, A161, A159, A219, A213, A214, A215, A216, A217, A218;
then A220: x2y < (x2y3 + x3y) - x3y3 by Th42;
x2y3 + (x3y + (- x3y3)) <= x1y3 + (x3y + (- x3y3)) by A211, Th32;
then (x2y3 + x3y) + (- x3y3) <= x1y3 + (x3y + (- x3y3)) by Th37;
then (x2y3 + x3y) + (- x3y3) <= (x1y3 + x3y) + (- x3y3) by Th37;
then A221: x2y < (x1y3 + x3y) + (- x3y3) by A220, SURREALO:4;
r = (x3y + x1y3) + (- x3y3) by A204;
hence not r <= l by A203, A221, TARSKI:def 1; :: thesis:

end;

suppose r in comp ((R_ x1),x1,y,(L_ y)) ; :: thesis:

then consider x3, y3 being Surreal such that
A222: ( r = ((x3 * y) +' (x1 * y3)) +' (-' (x3 * y3)) & x3 in R_ x1 & y3 in L_ y ) by Def14;
A223: ( {x1} << R_ x1 & x1 in {x1} ) by SURREALO:11, TARSKI:def 1;
A224: y3 in (L_ y) \/ (R_ y) by A222, XBOOLE_0:def 3;
then A225: ( (born x1) (+) (born y3) in (born x1) (+) (born y) & (born x2) (+) (born y3) in (born x2) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then reconsider x1y3 = x1 * y3, x2y3 = x2 * y3 as Surreal by A2, A162;
set BL = ((born x1) (+) (born y3)) \/ ((born x2) (+) (born y3));
x3 in (L_ x1) \/ (R_ x1) by A222, XBOOLE_0:def 3;
then A226: ( (born x3) (+) (born y3) in (born x1) (+) (born y3) & (born x3) (+) (born y) in (born x1) (+) (born y) ) by SURREALO:1, ORDINAL7:94;
then A227: ( (born x3) (+) (born y3) in D & (born x3) (+) (born y) in D ) by A225, A162, ORDINAL1:10;
then reconsider x3y3 = x3 * y3, x3y = x3 * y as Surreal by A2;
A228: ((born x1) (+) (born x2)) (+) (born y3) in ((born x1) (+) (born x2)) (+) (born y) by A224, SURREALO:1, ORDINAL7:94;
( (born x1) (+) (born y3) c= D & (born x2) (+) (born y3) c= D ) by A225, A162, ORDINAL1:def 2;
then A229: x1y3 == x2y3 by A228, A159, A161, A163;
((born y) (+) (born x3)) (+) (born x2) in ((born y) (+) (born x1)) (+) (born x2) by A226, ORDINAL7:94;
then A230: ((born y) (+) (born x3)) (+) (born x2) in (born y) (+) ((born x1) (+) (born x2)) by ORDINAL7:68;
A231: ((born y) (+) (born x3)) (+) (born x2) = ((born y) (+) (born x2)) (+) (born x3) by ORDINAL7:68;
A232: (born x2) (+) (born y3) c= D by A225, A162, ORDINAL1:def 2;
A233: y3 * x2 = x2y3 by A3, A225, A162, ORDINAL1:def 2;
A234: ( (born x3) (+) (born y) c= D & (born x2) (+) (born y) c= D ) by A226, A162, ORDINAL1:def 2;
A235: ( y * x3 = x3y & y * x2 = x2y ) by A163, A3, A226, A162, ORDINAL1:def 2;
A236: (born x3) (+) (born y3) c= D by A226, A225, A162, ORDINAL1:10, ORDINAL1:def 2;
A237: y3 * x3 = x3y3 by A3, A227, ORDINAL1:def 2;
A238: ( y3 < y & x2 < x3 ) by A223, A222, A163, SURREALO:4, A165;
x3y3 + x2y < x2y3 + x3y by A231, A222, A230, A159, A161, A238, A232, A233, A234, A235, A236, A237;
then A239: x2y < (x2y3 + x3y) - x3y3 by Th42;
x2y3 + (x3y + (- x3y3)) <= x1y3 + (x3y - x3y3) by A229, Th32;
then (x2y3 + x3y) - x3y3 <= x1y3 + (x3y - x3y3) by Th37;
then (x2y3 + x3y) - x3y3 <= (x1y3 + x3y) - x3y3 by Th37;
then A240: x2y < (x1y3 + x3y) - x3y3 by A239, SURREALO:4;
r = (x3y + x1y3) - x3y3 by A222;
hence not r <= l by A203, A240, TARSKI:def 1; :: thesis:

end;

end;

end;

end;

let x, y1, y2 be Surreal; :: thesis:
assume A241: ((born x) (+) (born y1)) (+) (born y2) c= E ; :: thesis:
thus S₃[D,x,y1,y2] :: thesis:

let x1y, x2y be Surreal; :: thesis:
assume A242: ( (born x) (+) (born y2) c= D & (born y1) (+) (born y2) c= D & x == y1 & x1y = x * y2 & x2y = y1 * y2 ) ; :: thesis:
A243: ( L_ x1y << {x2y} & {x2y} << R_ x1y & L_ x2y << {x1y} & {x1y} << R_ x2y ) by A241, A242, A160;
then reconsider z = [((L_ x1y) \/ (L_ x2y)),((R_ x1y) \/ (R_ x2y))] as Surreal by SURREALO:14;
( x1y == z & z == x2y ) by A243, SURREALO:15;
hence x1y == x2y by SURREALO:4; :: thesis:

end;

assume y1 < y2 ; :: thesis:

per cases by SURREALO:13;

suppose ex y2L being Surreal st
( y2L in L_ y2 & y1 <= y2L & y2L < y2 ) ; :: thesis:

then consider y2L being Surreal such that
A244: ( y2L in L_ y2 & y1 <= y2L & y2L < y2 ) ;
A245: for xL being Surreal st xL in L_ x holds
S₄[D,xL,x,y1,y2]

let xL be Surreal; :: thesis:
assume A246: xL in L_ x ; :: thesis:
let xLy2, xy1, xLy1, xy2 be Surreal; :: thesis:
assume that
A247: ( (born xL) (+) (born y1) c= D & (born x) (+) (born y1) c= D & (born xL) (+) (born y2) c= D & (born x) (+) (born y2) c= D ) and
A248: ( xLy1 = xL * y1 & xLy2 = xL * y2 & xy1 = x * y1 & xy2 = x * y2 ) and
A249: ( xL < x & y1 < y2 ) ; :: thesis:
A250: xy2 = [((comp ((L_ x),x,y2,(L_ y2))) \/ (comp ((R_ x),x,y2,(R_ y2)))),((comp ((L_ x),x,y2,(R_ y2))) \/ (comp ((R_ x),x,y2,(L_ y2))))] by A248, Th50;
A251: ( L_ xy2 << {xy2} & {xy2} << R_ xy2 & xy2 in {xy2} ) by SURREALO:11, TARSKI:def 1;
A252: y2L in (L_ y2) \/ (R_ y2) by A244, XBOOLE_0:def 3;
then A253: (born x) (+) (born y2L) in (born x) (+) (born y2) by SURREALO:1, ORDINAL7:94;
then reconsider xy2L = x * y2L as Surreal by A2, A247;
A254: xL in (L_ x) \/ (R_ x) by A246, XBOOLE_0:def 3;
then A255: (born xL) (+) (born y2L) in (born x) (+) (born y2L) by SURREALO:1, ORDINAL7:94;
then A256: (born xL) (+) (born y2L) in D by A247, A253, ORDINAL1:10;
then reconsider xLy2L = xL * y2L as Surreal by A2;
(xLy2 +' xy2L) +' (-' xLy2L) in comp ((L_ x),x,y2,(L_ y2)) by A246, A244, A248, Def14;
then (xLy2 +' xy2L) +' (-' xLy2L) in L_ xy2 by A250, XBOOLE_0:def 3;
then (xLy2 + xy2L) - xLy2L < xy2 by A251;
then A257: xLy2 + xy2L < xy2 + xLy2L by Th41;
A258: ((born y1) (+) (born y2)) (+) (born x) = ((born x) (+) (born y1)) (+) (born y2) by ORDINAL7:68;
A259: (born y2L) (+) (born x) c= D by A253, A247, ORDINAL1:def 2;
A260: ( y2L * x = xy2L & y1 * x = xy1 ) by A253, A247, A248, A3, ORDINAL1:def 2;
A261: (born y2L) (+) (born xL) c= D by A255, A247, A253, ORDINAL1:10, ORDINAL1:def 2;
A262: y2L * xL = xLy2L by A3, A256, ORDINAL1:def 2;
A263: y1 * xL = xLy1 by A247, A248, A3;
A264: (born y2L) (+) (born y1) in (born y1) (+) (born y2) by A252, SURREALO:1, ORDINAL7:94;
then A265: ((born y2L) (+) (born y1)) (+) (born x) in ((born y2) (+) (born y1)) (+) (born x) by ORDINAL7:94;
then A266: ((born y2L) (+) (born y1)) (+) (born x) in E by A241, A258;
( ((born y2L) (+) (born y1)) (+) (born xL) in ((born y2) (+) (born y1)) (+) (born xL) & ((born y2) (+) (born y1)) (+) (born xL) in ((born y2) (+) (born y1)) (+) (born x) ) by A254, SURREALO:1, A264, ORDINAL7:94;
then A267: ((born y2L) (+) (born y1)) (+) (born xL) in ((born y1) (+) (born y2)) (+) (born x) by ORDINAL1:10;

per cases by A244;

suppose A268: y1 < y2L ; :: thesis:

((born x) (+) (born y1)) (+) (born y2L) in E by A266, ORDINAL7:68;
then A269: xLy2L + xy1 <= xLy1 + xy2L by A246, A159, A249, A268, A261, A247, A248, A259;
A270: (xLy2L + xy1) + (xLy2 + xy2L) < (xLy1 + xy2L) + (xy2 + xLy2L) by A257, A269, Th44;
A271: (xLy2L + xy1) + (xLy2 + xy2L) = xLy2L + (xy1 + (xLy2 + xy2L)) by Th37
.= xLy2L + ((xy1 + xLy2) + xy2L) by Th37
.= (xLy2L + xy2L) + (xLy2 + xy1) by Th37 ;
(xLy1 + xy2L) + (xy2 + xLy2L) = xy2L + (xLy1 + (xy2 + xLy2L)) by Th37
.= xy2L + ((xLy1 + xy2) + xLy2L) by Th37
.= (xLy2L + xy2L) + (xLy1 + xy2) by Th37 ;
hence xLy2 + xy1 < xLy1 + xy2 by A270, A271, Th43; :: thesis:

end;

suppose A272: y1 == y2L ; :: thesis:

A273: xy2L == xy1 by A241, A258, A265, A159, A247, A259, A272, A260;
A274: xLy2L == xLy1 by A261, A263, A262, A247, A272, A267, A159, A241, A258;
A275: xy2 + xLy2L <= xLy1 + xy2 by A274, Th32;
A276: xLy2 + xy1 <= xLy2 + xy2L by A273, Th32;
xLy2 + xy1 < xy2 + xLy2L by A257, A276, SURREALO:4;
hence xLy2 + xy1 < xLy1 + xy2 by A275, SURREALO:4; :: thesis:

end;

end;

end;

for xR being Surreal st xR in R_ x holds
S₄[D,x,xR,y1,y2]

let xR be Surreal; :: thesis:
assume A277: xR in R_ x ; :: thesis:
let xy2, xRy1, xy1, xRy2 be Surreal; :: thesis:
assume that
A278: ( (born x) (+) (born y1) c= D & (born xR) (+) (born y1) c= D & (born x) (+) (born y2) c= D & (born xR) (+) (born y2) c= D ) and
A279: ( xy1 = x * y1 & xy2 = x * y2 & xRy1 = xR * y1 & xRy2 = xR * y2 ) and
A280: ( x < xR & y1 < y2 ) ; :: thesis:
A281: xy2 = [((comp ((L_ x),x,y2,(L_ y2))) \/ (comp ((R_ x),x,y2,(R_ y2)))),((comp ((L_ x),x,y2,(R_ y2))) \/ (comp ((R_ x),x,y2,(L_ y2))))] by A279, Th50;
A282: ( L_ xy2 << {xy2} & {xy2} << R_ xy2 & xy2 in {xy2} ) by SURREALO:11, TARSKI:def 1;
A283: y2L in (L_ y2) \/ (R_ y2) by A244, XBOOLE_0:def 3;
A284: (born x) (+) (born y2L) in (born x) (+) (born y2) by A283, SURREALO:1, ORDINAL7:94;
reconsider xy2L = x * y2L as Surreal by A2, A284, A278;
A285: xR in (L_ x) \/ (R_ x) by A277, XBOOLE_0:def 3;
A286: (born xR) (+) (born y2L) in (born x) (+) (born y2L) by A285, SURREALO:1, ORDINAL7:94;
then A287: (born xR) (+) (born y2L) in D by A278, A284, ORDINAL1:10;
then reconsider xRy2L = xR * y2L as Surreal by A2;
(xRy2 +' xy2L) +' (-' xRy2L) in comp ((R_ x),x,y2,(L_ y2)) by A277, A244, A279, Def14;
then (xRy2 +' xy2L) +' (-' xRy2L) in R_ xy2 by A281, XBOOLE_0:def 3;
then A288: xy2 < (xRy2 + xy2L) - xRy2L by A282;
then A289: xy2 + xRy2L < xRy2 + xy2L by Th42;
A290: ((born y1) (+) (born y2)) (+) (born x) = ((born x) (+) (born y1)) (+) (born y2) by ORDINAL7:68;
A291: (born y2L) (+) (born x) c= D by A284, A278, ORDINAL1:def 2;
A292: ( y2L * x = xy2L & y1 * x = xy1 ) by A284, A278, A279, A3, ORDINAL1:def 2;
A293: (born y2L) (+) (born xR) c= D by A286, A278, A284, ORDINAL1:10, ORDINAL1:def 2;
A294: y2L * xR = xRy2L by A3, A287, ORDINAL1:def 2;
A295: y1 * xR = xRy1 by A278, A279, A3;
A296: (born y2L) (+) (born y1) in (born y1) (+) (born y2) by A283, SURREALO:1, ORDINAL7:94;
then A297: ((born y2L) (+) (born y1)) (+) (born x) in ((born y1) (+) (born y2)) (+) (born x) by ORDINAL7:94;
then A298: ((born y2L) (+) (born y1)) (+) (born x) in E by A241, A290;
( ((born y2L) (+) (born y1)) (+) (born xR) in ((born y2) (+) (born y1)) (+) (born xR) & ((born y2) (+) (born y1)) (+) (born xR) in ((born y2) (+) (born y1)) (+) (born x) ) by A285, SURREALO:1, A296, ORDINAL7:94;
then A299: ((born y2L) (+) (born y1)) (+) (born xR) in ((born y1) (+) (born y2)) (+) (born x) by ORDINAL1:10;

per cases by A244;

suppose A300: y1 < y2L ; :: thesis:

((born x) (+) (born y1)) (+) (born y2L) in E by A298, ORDINAL7:68;
then A301: xy2L + xRy1 < xy1 + xRy2L by A277, A159, A280, A300, A293, A278, A279, A291;
xy2 + xRy2L <= xRy2 + xy2L by Th42, A288;
then A302: (xy2 + xRy2L) + (xy2L + xRy1) < (xRy2 + xy2L) + (xy1 + xRy2L) by A301, Th44;
A303: (xy2 + xRy2L) + (xy2L + xRy1) = xy2 + (xRy2L + (xy2L + xRy1)) by Th37
.= xy2 + ((xRy2L + xy2L) + xRy1) by Th37
.= (xy2 + xRy1) + (xRy2L + xy2L) by Th37 ;
(xRy2 + xy2L) + (xy1 + xRy2L) = xy2L + (xRy2 + (xy1 + xRy2L)) by Th37
.= xy2L + ((xRy2 + xy1) + xRy2L) by Th37
.= (xy1 + xRy2) + (xRy2L + xy2L) by Th37 ;
hence xy2 + xRy1 < xy1 + xRy2 by A303, A302, Th43; :: thesis:

end;

suppose A304: y1 == y2L ; :: thesis:

A305: xy1 == xy2L by A159, A297, A241, A290, A278, A291, A304, A292;
A306: xRy1 == xRy2L by A293, A295, A294, A278, A304, A299, A159, A241, A290;
A307: xy2 + xRy1 <= xy2 + xRy2L by A306, Th32;
A308: xRy2 + xy2L <= xy1 + xRy2 by A305, Th32;
xy2 + xRy1 < xRy2 + xy2L by A289, A307, SURREALO:4;
hence xy2 + xRy1 < xy1 + xRy2 by A308, SURREALO:4; :: thesis:

end;

end;

end;

hence ( ( for x being Surreal st x in L_ x holds
S₄[D,x,x,y1,y2] ) & ( for x being Surreal st x in R_ x holds
S₄[D,x,x,y1,y2] ) ) by A245; :: thesis:

end;

suppose ex y1R being Surreal st
( y1R in R_ y1 & y1 < y1R & y1R <= y2 ) ; :: thesis:

then consider y1R being Surreal such that
A309: ( y1R in R_ y1 & y1 < y1R & y1R <= y2 ) ;
A310: for xL being Surreal st xL in L_ x holds
S₄[D,xL,x,y1,y2]

let xL be Surreal; :: thesis:
assume A311: xL in L_ x ; :: thesis:
let xLy2, xy1, xLy1, xy2 be Surreal; :: thesis:
assume that
A312: ( (born xL) (+) (born y1) c= D & (born x) (+) (born y1) c= D & (born xL) (+) (born y2) c= D & (born x) (+) (born y2) c= D ) and
A313: ( xLy1 = xL * y1 & xLy2 = xL * y2 & xy1 = x * y1 & xy2 = x * y2 ) and
A314: ( xL < x & y1 < y2 ) ; :: thesis:
A315: xy1 = [((comp ((L_ x),x,y1,(L_ y1))) \/ (comp ((R_ x),x,y1,(R_ y1)))),((comp ((L_ x),x,y1,(R_ y1))) \/ (comp ((R_ x),x,y1,(L_ y1))))] by A313, Th50;
A316: ( L_ xy1 << {xy1} & {xy1} << R_ xy1 & xy1 in {xy1} ) by SURREALO:11, TARSKI:def 1;
A317: y1R in (L_ y1) \/ (R_ y1) by A309, XBOOLE_0:def 3;
A318: (born x) (+) (born y1R) in (born x) (+) (born y1) by A317, SURREALO:1, ORDINAL7:94;
reconsider xy1R = x * y1R as Surreal by A2, A312, A318;
A319: xL in (L_ x) \/ (R_ x) by A311, XBOOLE_0:def 3;
then A320: (born xL) (+) (born y1R) in (born x) (+) (born y1R) by SURREALO:1, ORDINAL7:94;
then A321: (born xL) (+) (born y1R) in (born x) (+) (born y1) by A318, ORDINAL1:10;
A322: (born xL) (+) (born y1R) in D by A320, A318, ORDINAL1:10, A312;
reconsider xLy1R = xL * y1R as Surreal by A321, A2, A312;
(xLy1 +' xy1R) +' (-' xLy1R) in comp ((L_ x),x,y1,(R_ y1)) by A311, A309, A313, Def14;
then (xLy1 +' xy1R) +' (-' xLy1R) in R_ xy1 by A315, XBOOLE_0:def 3;
then A323: xy1 < (xLy1 + xy1R) - xLy1R by A316;
then A324: xy1 + xLy1R < xLy1 + xy1R by Th42;
A325: ((born y1) (+) (born y2)) (+) (born x) = ((born x) (+) (born y1)) (+) (born y2) by ORDINAL7:68;
A326: (born y1R) (+) (born x) c= D by A318, A312, ORDINAL1:def 2;
A327: ( y1R * x = xy1R & y2 * x = xy2 ) by A318, A312, ORDINAL1:def 2, A313, A3;
A328: (born y1R) (+) (born xL) c= D by A320, A318, ORDINAL1:10, A312, ORDINAL1:def 2;
A329: y1R * xL = xLy1R by A3, A322, ORDINAL1:def 2;
A330: y2 * xL = xLy2 by A312, A313, A3;
A331: (born y1R) (+) (born y2) in (born y1) (+) (born y2) by A317, SURREALO:1, ORDINAL7:94;
then A332: ((born y1R) (+) (born y2)) (+) (born x) in ((born y1) (+) (born y2)) (+) (born x) by ORDINAL7:94;
then A333: ((born y1R) (+) (born y2)) (+) (born x) in E by A241, A325;
( ((born y1R) (+) (born y2)) (+) (born xL) in ((born y1) (+) (born y2)) (+) (born xL) & ((born y1) (+) (born y2)) (+) (born xL) in ((born y1) (+) (born y2)) (+) (born x) ) by A319, SURREALO:1, A331, ORDINAL7:94;
then A334: ((born y1R) (+) (born y2)) (+) (born xL) in ((born y1) (+) (born y2)) (+) (born x) by ORDINAL1:10;

per cases by A309;

suppose A335: y1R < y2 ; :: thesis:

((born x) (+) (born y1R)) (+) (born y2) in E by A333, ORDINAL7:68;
then A336: xLy2 + xy1R < xLy1R + xy2 by A159, A311, A314, A335, A328, A312, A313, A326;
xy1 + xLy1R <= xLy1 + xy1R by A323, Th42;
then A337: (xy1 + xLy1R) + (xLy2 + xy1R) < (xLy1 + xy1R) + (xLy1R + xy2) by A336, Th44;
A338: (xy1 + xLy1R) + (xLy2 + xy1R) = xy1 + (xLy1R + (xLy2 + xy1R)) by Th37
.= xy1 + (xLy2 + (xLy1R + xy1R)) by Th37
.= (xy1 + xLy2) + (xLy1R + xy1R) by Th37 ;
(xLy1 + xy1R) + (xLy1R + xy2) = xLy1 + (xy1R + (xLy1R + xy2)) by Th37
.= xLy1 + ((xy1R + xLy1R) + xy2) by Th37
.= (xLy1 + xy2) + (xy1R + xLy1R) by Th37 ;
hence xLy2 + xy1 < xLy1 + xy2 by A337, A338, Th43; :: thesis:

end;

suppose A339: y1R == y2 ; :: thesis:

A340: xy1R == xy2 by A332, A241, A325, A159, A312, A326, A339, A327;
A341: xLy1R == xLy2 by A328, A330, A329, A312, A339, A334, A159, A241, A325;
A342: xy1 + xLy2 <= xy1 + xLy1R by A341, Th32;
A343: xLy1 + xy1R <= xLy1 + xy2 by A340, Th32;
xy1 + xLy2 < xLy1 + xy1R by A324, A342, SURREALO:4;
hence xLy2 + xy1 < xLy1 + xy2 by A343, SURREALO:4; :: thesis:

end;

end;

end;

for xR being Surreal st xR in R_ x holds
S₄[D,x,xR,y1,y2]

let xR be Surreal; :: thesis:
assume A344: xR in R_ x ; :: thesis:
let xy2, xRy1, xy1, xRy2 be Surreal; :: thesis:
assume that
A345: ( (born x) (+) (born y1) c= D & (born xR) (+) (born y1) c= D & (born x) (+) (born y2) c= D & (born xR) (+) (born y2) c= D ) and
A346: ( xy1 = x * y1 & xy2 = x * y2 & xRy1 = xR * y1 & xRy2 = xR * y2 ) and
A347: ( x < xR & y1 < y2 ) ; :: thesis:
A348: xy1 = [((comp ((L_ x),x,y1,(L_ y1))) \/ (comp ((R_ x),x,y1,(R_ y1)))),((comp ((L_ x),x,y1,(R_ y1))) \/ (comp ((R_ x),x,y1,(L_ y1))))] by A346, Th50;
A349: ( L_ xy1 << {xy1} & {xy1} << R_ xy1 & xy1 in {xy1} ) by SURREALO:11, TARSKI:def 1;
A350: y1R in (L_ y1) \/ (R_ y1) by A309, XBOOLE_0:def 3;
A351: (born x) (+) (born y1R) in (born x) (+) (born y1) by SURREALO:1, A350, ORDINAL7:94;
then reconsider xy1R = x * y1R as Surreal by A2, A345;
A352: xR in (L_ x) \/ (R_ x) by A344, XBOOLE_0:def 3;
A353: (born xR) (+) (born y1R) in (born x) (+) (born y1R) by A352, SURREALO:1, ORDINAL7:94;
then A354: (born xR) (+) (born y1R) in D by A345, A351, ORDINAL1:10;
then reconsider xRy1R = xR * y1R as Surreal by A2;
(xRy1 +' xy1R) +' (-' xRy1R) in comp ((R_ x),x,y1,(R_ y1)) by A344, A309, A346, Def14;
then (xRy1 +' xy1R) +' (-' xRy1R) in L_ xy1 by A348, XBOOLE_0:def 3;
then A355: (xRy1 + xy1R) - xRy1R < xy1 by A349;
then A356: xRy1 + xy1R < xy1 + xRy1R by Th41;
A357: ((born y1) (+) (born y2)) (+) (born x) = ((born x) (+) (born y1)) (+) (born y2) by ORDINAL7:68;
A358: (born y1R) (+) (born x) c= D by A351, A345, ORDINAL1:def 2;
A359: ( y1R * x = xy1R & y2 * x = xy2 ) by A345, A346, A3, A351, ORDINAL1:def 2;
A360: (born y1R) (+) (born xR) c= D by A353, A345, A351, ORDINAL1:10, ORDINAL1:def 2;
A361: y1R * xR = xRy1R by A3, A354, ORDINAL1:def 2;
A362: y2 * xR = xRy2 by A345, A346, A3;
A363: (born y1R) (+) (born y2) in (born y1) (+) (born y2) by A350, SURREALO:1, ORDINAL7:94;
then A364: ((born y1R) (+) (born y2)) (+) (born x) in ((born y1) (+) (born y2)) (+) (born x) by ORDINAL7:94;
then A365: ((born y1R) (+) (born y2)) (+) (born x) in E by A241, A357;
( ((born y1R) (+) (born y2)) (+) (born xR) in ((born y1) (+) (born y2)) (+) (born xR) & ((born y1) (+) (born y2)) (+) (born xR) in ((born y1) (+) (born y2)) (+) (born x) ) by A352, SURREALO:1, A363, ORDINAL7:94;
then A366: ((born y1R) (+) (born y2)) (+) (born xR) in ((born y1) (+) (born y2)) (+) (born x) by ORDINAL1:10;

per cases by A309;

suppose A367: y1R < y2 ; :: thesis:

((born x) (+) (born y1R)) (+) (born y2) in E by A365, ORDINAL7:68;
then A368: xy2 + xRy1R < xy1R + xRy2 by A344, A159, A347, A367, A360, A345, A346, A358;
xRy1 + xy1R <= xy1 + xRy1R by A355, Th41;
then A369: (xRy1 + xy1R) + (xy2 + xRy1R) < (xy1 + xRy1R) + (xy1R + xRy2) by A368, Th44;
A370: (xRy1 + xy1R) + (xy2 + xRy1R) = xRy1 + (xy1R + (xRy1R + xy2)) by Th37
.= xRy1 + ((xy1R + xRy1R) + xy2) by Th37
.= (xy1R + xRy1R) + (xy2 + xRy1) by Th37 ;
(xy1 + xRy1R) + (xy1R + xRy2) = xy1 + (xRy1R + (xy1R + xRy2)) by Th37
.= xy1 + ((xRy1R + xy1R) + xRy2) by Th37
.= (xy1 + xRy2) + (xRy1R + xy1R) by Th37 ;
hence xy2 + xRy1 < xy1 + xRy2 by A370, A369, Th43; :: thesis:

end;

suppose A371: y1R == y2 ; :: thesis:

A372: xy1R == xy2 by A159, A364, A241, A357, A345, A358, A371, A359;
A373: xRy1R == xRy2 by A360, A362, A361, A345, A371, A366, A159, A241, A357;
A374: xy1 + xRy1R <= xy1 + xRy2 by A373, Th32;
A375: xy2 + xRy1 <= xy1R + xRy1 by A372, Th32;
xRy1 + xy1R < xy1 + xRy2 by A356, A374, SURREALO:4;
hence xy2 + xRy1 < xy1 + xRy2 by A375, SURREALO:4; :: thesis:

end;

end;

end;

hence ( ( for x being Surreal st x in L_ x holds
S₄[D,x,x,y1,y2] ) & ( for x being Surreal st x in R_ x holds
S₄[D,x,x,y1,y2] ) ) by A310; :: thesis:

end;

end;

end;

A376: for E being Ordinal holds S₁₁[E] from ORDINAL1:sch 2(A158);
thus for x1, x2, y being Surreal holds S₃[D,x1,x2,y] :: thesis:

let x1, x2, y be Surreal; :: thesis:
((born x1) (+) (born x2)) (+) (born y) c= ((born x1) (+) (born x2)) (+) (born y) ;
hence S₃[D,x1,x2,y] by A376; :: thesis:

end;

defpred S₁₂[ Ordinal] means for x1, x2, y1, y2 being Surreal st (born x1) (+) (born x2) c= $1 holds
S₄[D,x1,x2,y1,y2];
A377: for E being Ordinal st ( for C being Ordinal st C in E holds
S₁₂[C] ) holds
S₁₂[E]

let E be Ordinal; :: thesis:
assume A378: for C being Ordinal st C in E holds
S₁₂[C] ; :: thesis:
let x1, x2, y1, y2 be Surreal; :: thesis:
assume A379: (born x1) (+) (born x2) c= E ; :: thesis:
let x1y2, x2y1, x1y1, x2y2 be Surreal; :: thesis:
assume that
A380: ( (born x1) (+) (born y1) c= D & (born x2) (+) (born y1) c= D & (born x1) (+) (born y2) c= D & (born x2) (+) (born y2) c= D ) and
A381: ( x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 ) ; :: thesis:

per cases by A381, SURREALO:13;

suppose ex x1R being Surreal st
( x1R in R_ x1 & x1 < x1R & x1R <= x2 ) ; :: thesis:

then consider x1R being Surreal such that
A382: ( x1R in R_ x1 & x1 < x1R & x1R <= x2 ) ;
x1R in (L_ x1) \/ (R_ x1) by A382, XBOOLE_0:def 3;
then A383: ( (born x1R) (+) (born x2) in (born x1) (+) (born x2) & (born x1R) (+) (born y1) in (born x1) (+) (born y1) & (born x1R) (+) (born y2) in (born x1) (+) (born y2) ) by SURREALO:1, ORDINAL7:94;
then reconsider x1Ry1 = x1R * y1, x1Ry2 = x1R * y2 as Surreal by A2, A380;
A384: ( (born x1R) (+) (born y1) c= D & (born x1R) (+) (born y2) c= D ) by A383, A380, ORDINAL1:def 2;

per cases by A382;

suppose A385: x1R == x2 ; :: thesis:

((born x1R) (+) (born x2)) (+) (born y1) c= ((born x1R) (+) (born x2)) (+) (born y1) ;
then A386: x1Ry1 == x2y1 by A376, A385, A384, A380, A381;
((born x1R) (+) (born x2)) (+) (born y2) c= ((born x1R) (+) (born x2)) (+) (born y2) ;
then A387: x1Ry2 == x2y2 by A376, A385, A384, A380, A381;
((born x1) (+) (born y1)) (+) (born y2) c= ((born x1) (+) (born y1)) (+) (born y2) ;
then A388: x1y2 + x1Ry1 < x1y1 + x1Ry2 by A376, A382, A380, A381, A384;
A389: x1y1 + x1Ry2 <= x1y1 + x2y2 by A387, Th32;
x1y2 + x2y1 <= x1y2 + x1Ry1 by A386, Th32;
then x1y2 + x2y1 < x1y1 + x1Ry2 by A388, SURREALO:4;
hence x1y2 + x2y1 < x1y1 + x2y2 by SURREALO:4, A389; :: thesis:

end;

suppose x1R < x2 ; :: thesis:

then A390: x1Ry2 + x2y1 < x1Ry1 + x2y2 by A384, A383, A378, A379, A380, A381;
((born x1) (+) (born y1)) (+) (born y2) c= ((born x1) (+) (born y1)) (+) (born y2) ;
then x1y2 + x1Ry1 <= x1y1 + x1Ry2 by A376, A384, A382, A380, A381;
then A391: (x1Ry2 + x2y1) + (x1y2 + x1Ry1) < (x1Ry1 + x2y2) + (x1y1 + x1Ry2) by A390, Th44;
A392: (x1Ry2 + x2y1) + (x1y2 + x1Ry1) = x1Ry2 + (x2y1 + (x1y2 + x1Ry1)) by Th37
.= x1Ry2 + ((x2y1 + x1y2) + x1Ry1) by Th37
.= (x1Ry2 + x1Ry1) + (x1y2 + x2y1) by Th37 ;
(x1Ry1 + x2y2) + (x1y1 + x1Ry2) = x1Ry1 + (x2y2 + (x1y1 + x1Ry2)) by Th37
.= x1Ry1 + ((x2y2 + x1y1) + x1Ry2) by Th37
.= (x1Ry1 + x1Ry2) + (x2y2 + x1y1) by Th37 ;
hence x1y2 + x2y1 < x1y1 + x2y2 by A391, A392, Th43; :: thesis:

end;

end;

end;

suppose ex x2L being Surreal st
( x2L in L_ x2 & x1 <= x2L & x2L < x2 ) ; :: thesis:

then consider x2L being Surreal such that
A393: ( x2L in L_ x2 & x1 <= x2L & x2L < x2 ) ;
x2L in (L_ x2) \/ (R_ x2) by A393, XBOOLE_0:def 3;
then A394: ( (born x2L) (+) (born x1) in (born x1) (+) (born x2) & (born x2L) (+) (born y1) in (born x2) (+) (born y1) & (born x2L) (+) (born y2) in (born x2) (+) (born y2) ) by SURREALO:1, ORDINAL7:94;
then reconsider x2Ly1 = x2L * y1, x2Ly2 = x2L * y2 as Surreal by A2, A380;
A395: ( (born x2L) (+) (born y1) c= D & (born x2L) (+) (born y2) c= D ) by A394, A380, ORDINAL1:def 2;

per cases by A393;

suppose A396: x1 == x2L ; :: thesis:

((born x1) (+) (born x2L)) (+) (born y1) c= ((born x1) (+) (born x2L)) (+) (born y1) ;
then A397: x1y1 == x2Ly1 by A376, A396, A395, A380, A381;
((born x1) (+) (born x2L)) (+) (born y2) c= ((born x1) (+) (born x2L)) (+) (born y2) ;
then A398: x1y2 == x2Ly2 by A376, A396, A395, A380, A381;
((born x2) (+) (born y1)) (+) (born y2) c= ((born x2) (+) (born y1)) (+) (born y2) ;
then A399: x2Ly2 + x2y1 < x2Ly1 + x2y2 by A376, A393, A380, A381, A395;
A400: x2Ly1 + x2y2 <= x1y1 + x2y2 by A397, Th32;
x1y2 + x2y1 <= x2Ly2 + x2y1 by A398, Th32;
then x1y2 + x2y1 < x2Ly1 + x2y2 by A399, SURREALO:4;
hence x1y2 + x2y1 < x1y1 + x2y2 by A400, SURREALO:4; :: thesis:

end;

suppose x1 < x2L ; :: thesis:

then A401: x1y2 + x2Ly1 < x1y1 + x2Ly2 by A395, A394, A378, A379, A380, A381;
((born x2) (+) (born y1)) (+) (born y2) c= ((born x2) (+) (born y1)) (+) (born y2) ;
then x2Ly2 + x2y1 <= x2Ly1 + x2y2 by A376, A395, A393, A380, A381;
then A402: (x2Ly2 + x2y1) + (x1y2 + x2Ly1) < (x2Ly1 + x2y2) + (x1y1 + x2Ly2) by A401, Th44;
A403: (x2Ly2 + x2y1) + (x1y2 + x2Ly1) = x2Ly2 + (x2y1 + (x1y2 + x2Ly1)) by Th37
.= x2Ly2 + ((x2y1 + x1y2) + x2Ly1) by Th37
.= (x1y2 + x2y1) + (x2Ly2 + x2Ly1) by Th37 ;
(x2Ly1 + x2y2) + (x1y1 + x2Ly2) = x2Ly1 + (x2y2 + (x1y1 + x2Ly2)) by Th37
.= x2Ly1 + ((x2y2 + x1y1) + x2Ly2) by Th37
.= (x1y1 + x2y2) + (x2Ly2 + x2Ly1) by Th37 ;
hence x1y2 + x2y1 < x1y1 + x2y2 by A402, A403, Th43; :: thesis:

end;

end;

end;

end;

end;

A404: for E being Ordinal holds S₁₂[E] from ORDINAL1:sch 2(A377);
let x1, x2, y1, y2 be Surreal; :: thesis:
(born x1) (+) (born x2) c= (born x1) (+) (born x2) ;
hence S₄[D,x1,x2,y1,y2] by A404; :: thesis:

end;

A405: for E being Ordinal holds S₁₀[E] from ORDINAL1:sch 2(A1);
thus for x, y being Surreal holds x * y is Surreal by A405; :: thesis:
thus for x, y being Surreal holds x * y = y * x by A405; :: thesis:
thus for x1, x2, y, x1y, x2y being Surreal st x1 == x2 & x1y = x1 * y & x2y = x2 * y holds
x1y == x2y :: thesis:

let x1, x2, y, x1y, x2y be Surreal; :: thesis:
assume A406: ( x1 == x2 & x1y = x1 * y & x2y = x2 * y ) ; :: thesis:
set B1 = (born x1) (+) (born y);
set B2 = (born x2) (+) (born y);
set B = ((born x1) (+) (born y)) \/ ((born x2) (+) (born y));
( (born x1) (+) (born y) c= ((born x1) (+) (born y)) \/ ((born x2) (+) (born y)) & (born x2) (+) (born y) c= ((born x1) (+) (born y)) \/ ((born x2) (+) (born y)) ) by XBOOLE_1:7;
hence x1y == x2y by A406, A405; :: thesis:

end;

let x1, x2, y1, y2, x1y2, x2y1, x1y1, x2y2 be Surreal; :: thesis:
assume A407: ( x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 ) ; :: thesis:
set B11 = (born x1) (+) (born y1);
set B12 = (born x1) (+) (born y2);
set B21 = (born x2) (+) (born y1);
set B22 = (born x2) (+) (born y2);
set B1 = ((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2));
set B2 = ((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2));
set B = (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2)));
( (born x1) (+) (born y1) c= ((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2)) & (born x1) (+) (born y2) c= ((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2)) & (born x2) (+) (born y1) c= ((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2)) & (born x2) (+) (born y2) c= ((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2)) & ((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2)) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) & ((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2)) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) ) by XBOOLE_1:7;
then ( (born x1) (+) (born y1) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) & (born x1) (+) (born y2) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) & (born x2) (+) (born y1) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) & (born x2) (+) (born y2) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) ) by XBOOLE_1:1;
hence x1y2 + x2y1 < x1y1 + x2y2 by A405, A407; :: thesis: