defpred S₁[ Ordinal] means for x being Surreal st born x = $1 & x is positive holds
( inv x is surreal & ( for y being Surreal st y = inv x holds
x * y == 1_No ) );
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:
let x be Surreal; :: thesis:
assume A3: ( born x = D & x is positive ) ; :: thesis:
set Nx = ||.x.||;
set Inv = No_inverses_on ||.x.||;
A4: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A3, Th20;
A5: No_inverses_on ||.x.|| is ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} -surreal-valued

let o be object ; :: according to SURREALI:def 7 :: thesis:
assume A6: o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( born o in born x & o is positive ) by A6, A4, A3, SURREALO:1, Th21;
then inv o is surreal by A2, A3;
hence (No_inverses_on ||.x.||) . o is Surreal by A6, Def13; :: thesis:

end;

then A7: ( Union (divL (||.x.||,(No_inverses_on ||.x.||))) is surreal-membered & Union (divR (||.x.||,(No_inverses_on ||.x.||))) is surreal-membered ) by Th10;
defpred S₂[ Nat] means ( ( for yL being Surreal st yL in (divL (||.x.||,(No_inverses_on ||.x.||))) . $1 holds
||.x.|| * yL < 1_No ) & ( for yR being Surreal st yR in (divR (||.x.||,(No_inverses_on ||.x.||))) . $1 holds
1_No < ||.x.|| * yR ) );
A8: S₂[ 0 ]

proof

thus for yL being Surreal st yL in (divL (||.x.||,(No_inverses_on ||.x.||))) . 0 holds
||.x.|| * yL < 1_No :: thesis:

proof

A9: 1_No is positive ;
let yL be Surreal; :: thesis:
assume A10: yL in (divL (||.x.||,(No_inverses_on ||.x.||))) . 0 ; :: thesis:
(divL (||.x.||,(No_inverses_on ||.x.||))) . 0 = {0_No} by Th1;
then yL = 0_No by A10, TARSKI:def 1;
hence ||.x.|| * yL < 1_No by A9; :: thesis:

end;

thus for yR being Surreal st yR in (divR (||.x.||,(No_inverses_on ||.x.||))) . 0 holds
1_No < ||.x.|| * yR by Th1; :: thesis:

end;

A11: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume A12: S₂[n] ; :: thesis:
set n1 = n + 1;
A13: ( (divL (||.x.||,(No_inverses_on ||.x.||))) . n c= Union (divL (||.x.||,(No_inverses_on ||.x.||))) & (divR (||.x.||,(No_inverses_on ||.x.||))) . n c= Union (divR (||.x.||,(No_inverses_on ||.x.||))) ) by ABCMIZ_1:1;
thus for yL being Surreal st yL in (divL (||.x.||,(No_inverses_on ||.x.||))) . (n + 1) holds
||.x.|| * yL < 1_No :: thesis:

proof

per cases by XBOOLE_0:def 3;

suppose yL in (divL (||.x.||,(No_inverses_on ||.x.||))) . n ; :: thesis:

hence ||.x.|| * yL < 1_No by A12; :: thesis:

end;

suppose yL in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

end;

suppose yL in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

end;

per cases by XBOOLE_0:def 3;

suppose yL in (divR (||.x.||,(No_inverses_on ||.x.||))) . n ; :: thesis:

hence 1_No < ||.x.|| * yL by A12; :: thesis:

end;

suppose yL in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

end;

suppose yL in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

end;

A92: for n being Nat holds S₂[n] from NAT_1:sch 2(A8, A11);
A93: 0_No <= ||.x.|| by Def8;
A94: Union (divL (||.x.||,(No_inverses_on ||.x.||))) << Union (divR (||.x.||,(No_inverses_on ||.x.||)))

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A95: ( l in Union (divL (||.x.||,(No_inverses_on ||.x.||))) & r in Union (divR (||.x.||,(No_inverses_on ||.x.||))) ) ; :: thesis:
dom (divL (||.x.||,(No_inverses_on ||.x.||))) = NAT by Def5;
then consider n1 being Nat such that
A96: ( l in (divL (||.x.||,(No_inverses_on ||.x.||))) . n1 & ( for m being Nat st l in (divL (||.x.||,(No_inverses_on ||.x.||))) . m holds
n1 <= m ) ) by A95, Th27;
dom (divR (||.x.||,(No_inverses_on ||.x.||))) = NAT by Def6;
then consider n2 being Nat such that
A97: ( r in (divR (||.x.||,(No_inverses_on ||.x.||))) . n2 & ( for m being Nat st r in (divR (||.x.||,(No_inverses_on ||.x.||))) . m holds
n2 <= m ) ) by A95, Th27;
n2 <> 0 by A97, Th1;
then reconsider N2 = n2 - 1 as Nat by NAT_1:20;

per cases ;

suppose n1 = 0 ; :: thesis:

then {0_No} = (divL (||.x.||,(No_inverses_on ||.x.||))) . n1 by Th1;
then A98: l = 0_No by A96, TARSKI:def 1;
( 0_No <= 1_No & 1_No < ||.x.|| * r ) by A92, A97, Def8;
then 0_No < ||.x.|| * r by SURREALO:4;
hence not r <= l by A98, A93, SURREALR:72; :: thesis:

end;

suppose 0 < n1 ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose l in (divL (||.x.||,(No_inverses_on ||.x.||))) . N1 ; :: thesis:

then N1 >= N1 + 1 by A96;
hence not r <= l by NAT_1:13; :: thesis:

end;

suppose l in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . N1),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose r in (divR (||.x.||,(No_inverses_on ||.x.||))) . N2 ; :: thesis:

then N2 >= N2 + 1 by A97;
hence not r <= l by NAT_1:13; :: thesis:

end;

suppose r in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider y2 being object such that
A106: ( y2 in (divL (||.x.||,(No_inverses_on ||.x.||))) . N2 & r in divs (y2,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider y2 = y2 as Surreal by A7, A106, A99;
consider x2 being object such that
A107: ( x2 in L_ ||.x.|| & x2 <> 0_No & r = (1_No +' ((x2 +' (-' ||.x.||)) *' y2)) *' ((No_inverses_on ||.x.||) . x2) ) by A106, Def2;
reconsider x2 = x2 as Surreal by A107, SURREAL0:def 16;
A108: ( x2 is positive & x2 in L_ x ) by A3, Def9, A107;
then ( 0_No < x2 & x2 in (L_ x) \/ (R_ x) ) by XBOOLE_0:def 3;
then A109: born x2 in born x by SURREALO:1;
then reconsider Ix2 = inv x2 as Surreal by A108, A3, A2;
A110: x2 * Ix2 == 1_No by A3, A2, A109, A108;
x2 in (L_ ||.x.||) \/ (R_ ||.x.||) by A107, XBOOLE_0:def 3;
then A111: x2 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A107, ZFMISC_1:56;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

proof

( L_ ||.x.|| << {||.x.||} & {||.x.||} << R_ ||.x.|| & ||.x.|| in {||.x.||} ) by TARSKI:def 1, SURREALO:11;
then A112: ( 0_No < x1 - ||.x.|| & 0_No < ||.x.|| - x2 ) by SURREALR:45, A101, A107;
L_ ||.x.|| << R_ ||.x.|| by SURREAL0:45;
then A113: 0_No < x1 - x2 by A107, A101, SURREALR:45;
A114: ( 0_No < 1_No - (||.x.|| * y1) & 0_No < 1_No - (||.x.|| * y2) ) by A100, A106, A92, SURREALR:45;
A115: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y1))) + (((y1 - y2) * x1) * (||.x.|| - x2)) by Th29;
A116: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y2))) + (((y2 - y1) * x2) * (x1 - ||.x.||)) by Th29;
A117: ( x2 is positive & x1 is positive ) by A3, A107, A101, Def9;
A118: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y1))) by A113, A114, SURREALR:72;
A119: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y2))) by A113, A114, SURREALR:72;

per cases ;

suppose y1 == y2 ; :: thesis:

then ( y1 + (- y2) == y2 - y2 & y2 - y2 == 0_No ) by SURREALR:43, SURREALR:39;
then y1 + (- y2) == 0_No by SURREALO:4;
then ( (y1 + (- y2)) * x1 == 0_No * x1 & 0_No * x1 = 0_No ) by SURREALR:51;
then ( ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) == 0_No * (||.x.|| + (- x2)) & 0_No * (||.x.|| + (- x2)) = 0_No ) by SURREALR:51;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) by A118, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A115, SURREALO:4; :: thesis:

end;

suppose y1 < y2 ; :: thesis:

then 0_No < y2 - y1 by SURREALR:45;
then 0_No < (y2 + (- y1)) * x2 by A117, SURREALR:72;
then 0_No <= ((y2 + (- y1)) * x2) * (x1 + (- ||.x.||)) by A112, SURREALR:72;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- ||.x.||))) by A119, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A116, SURREALO:4; :: thesis:

end;

suppose y2 < y1 ; :: thesis:

then 0_No < y1 - y2 by SURREALR:45;
then 0_No < (y1 + (- y2)) * x1 by A117, SURREALR:72;
then 0_No <= ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) by A112, SURREALR:72;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) by A118, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A115, SURREALO:4; :: thesis:

end;

then (1_No + ((x1 + (- ||.x.||)) * y1)) * x2 < (1_No + ((x2 + (- ||.x.||)) * y2)) * x1 by SURREALR:45;
then (1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1 < (1_No + ((x2 + (- ||.x.||)) * y2)) * Ix2 by A108, A102, A104, A110, Th28;
hence not r <= l by A101, A107, A105, A111, Def13; :: thesis:

end;

suppose r in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider y2 being object such that
A120: ( y2 in (divR (||.x.||,(No_inverses_on ||.x.||))) . N2 & r in divs (y2,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider y2 = y2 as Surreal by A7, A120, A99;
consider x2 being object such that
A121: ( x2 in R_ ||.x.|| & x2 <> 0_No & r = (1_No +' ((x2 +' (-' ||.x.||)) *' y2)) *' ((No_inverses_on ||.x.||) . x2) ) by A120, Def2;
reconsider x2 = x2 as Surreal by A121, SURREAL0:def 16;
A122: ( x2 is positive & x2 in R_ x ) by A3, Def9, A121;
then ( 0_No < x2 & x2 in (L_ x) \/ (R_ x) ) by XBOOLE_0:def 3;
then A123: born x2 in born x by SURREALO:1;
then reconsider Ix2 = inv x2 as Surreal by A122, A3, A2;
A124: x2 * Ix2 == 1_No by A3, A2, A123, A122;
x2 in (L_ ||.x.||) \/ (R_ ||.x.||) by A121, XBOOLE_0:def 3;
then A125: x2 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A121, ZFMISC_1:56;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

proof

( L_ ||.x.|| << {||.x.||} & {||.x.||} << R_ ||.x.|| & ||.x.|| in {||.x.||} ) by TARSKI:def 1, SURREALO:11;
then A126: ( 0_No < x1 - ||.x.|| & ||.x.|| - x2 < 0_No ) by A101, A121, SURREALR:45, SURREALR:46;
( ||.x.|| * y1 < 1_No & 1_No <= ||.x.|| * y2 ) by A100, A120, A92;
then ||.x.|| * y1 < ||.x.|| * y2 by SURREALO:4;
then y1 < y2 by Def8, SURREALR:73;
then A127: ( y1 - y2 < 0_No & 0_No < y2 - y1 ) by SURREALR:45, SURREALR:46;
A128: 1_No - (||.x.|| * y2) < 0_No by A120, A92, SURREALR:46;
A129: ( 0_No < 1_No - (||.x.|| * y1) & 0_No < (||.x.|| * y2) - 1_No ) by A100, A120, A92, SURREALR:45;
A130: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y1))) + (((y1 - y2) * x1) * (||.x.|| - x2)) by Th29;
A131: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y2))) + (((y2 - y1) * x2) * (x1 - ||.x.||)) by Th29;
A132: ( x2 is positive & x1 is positive ) by A3, A121, A101, Def9;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

proof

A133: ((y1 + (- y2)) * (||.x.|| + (- x2))) * x1 == ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) by SURREALR:69;
0_No < (y1 + (- y2)) * (||.x.|| + (- x2)) by A127, A126, SURREALR:72;
then 0_No < ((y1 + (- y2)) * (||.x.|| + (- x2))) * x1 by A132, SURREALR:72;
then A134: 0_No < ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) by A133, SURREALO:4;

per cases ;

suppose x2 < x1 ; :: thesis:

then 0_No < x1 - x2 by SURREALR:45;
then A135: 0_No <= (x1 + (- x2)) * (1_No + (- (||.x.|| * y1))) by A129, SURREALR:72;
0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) by A134, A135, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A130, SURREALO:4; :: thesis:

end;

suppose x1 == x2 ; :: thesis:

then ( x1 + (- x2) == x2 + (- x2) & x2 + (- x2) = x2 - x2 & x2 - x2 == 0_No ) by SURREALR:43, SURREALR:39;
then x1 + (- x2) == 0_No by SURREALO:4;
then ( (x1 + (- x2)) * (1_No + (- (||.x.|| * y1))) == 0_No * (1_No + (- (||.x.|| * y1))) & 0_No * (1_No + (- (||.x.|| * y1))) = 0_No ) by SURREALR:51;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) by A134, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A130, SURREALO:4; :: thesis:

end;

suppose x1 < x2 ; :: thesis:

then x1 - x2 < 0_No by SURREALR:46;
then A136: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y2))) by A128, SURREALR:72;
0_No < (y2 + (- y1)) * x2 by A127, A132, SURREALR:72;
then 0_No <= ((y2 + (- y1)) * x2) * (x1 + (- ||.x.||)) by A126, SURREALR:72;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- ||.x.||))) by A136, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A131, SURREALO:4; :: thesis:

end;

hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) ; :: thesis:

end;

then (1_No + ((x1 + (- ||.x.||)) * y1)) * x2 < (1_No + ((x2 + (- ||.x.||)) * y2)) * x1 by SURREALR:45;
then (1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1 < (1_No + ((x2 + (- ||.x.||)) * y2)) * Ix2 by A122, A102, A104, A124, Th28;
hence not r <= l by A101, A121, A105, A125, Def13; :: thesis:

end;

suppose l in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . N1),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose r in (divR (||.x.||,(No_inverses_on ||.x.||))) . N2 ; :: thesis:

then N2 >= N2 + 1 by A97;
hence not r <= l by NAT_1:13; :: thesis:

end;

suppose r in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider y2 being object such that
A143: ( y2 in (divL (||.x.||,(No_inverses_on ||.x.||))) . N2 & r in divs (y2,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider y2 = y2 as Surreal by A7, A143, A99;
consider x2 being object such that
A144: ( x2 in L_ ||.x.|| & x2 <> 0_No & r = (1_No +' ((x2 +' (-' ||.x.||)) *' y2)) *' ((No_inverses_on ||.x.||) . x2) ) by A143, Def2;
reconsider x2 = x2 as Surreal by A144, SURREAL0:def 16;
A145: ( x2 is positive & x2 in L_ x ) by A3, Def9, A144;
then ( 0_No < x2 & x2 in (L_ x) \/ (R_ x) ) by XBOOLE_0:def 3;
then A146: born x2 in born x by SURREALO:1;
then reconsider Ix2 = inv x2 as Surreal by A145, A3, A2;
A147: x2 * Ix2 == 1_No by A3, A2, A146, A145;
x2 in (L_ ||.x.||) \/ (R_ ||.x.||) by A144, XBOOLE_0:def 3;
then A148: x2 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A144, ZFMISC_1:56;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

proof

( L_ ||.x.|| << {||.x.||} & {||.x.||} << R_ ||.x.|| & ||.x.|| in {||.x.||} ) by TARSKI:def 1, SURREALO:11;
then A149: ( x1 - ||.x.|| < 0_No & x2 - ||.x.|| < 0_No & 0_No < ||.x.|| - x2 ) by A138, A144, SURREALR:45, SURREALR:46;
( ||.x.|| * y2 < 1_No & 1_No <= ||.x.|| * y1 ) by A137, A143, A92;
then ||.x.|| * y2 < ||.x.|| * y1 by SURREALO:4;
then y2 < y1 by Def8, SURREALR:73;
then A150: ( y2 - y1 < 0_No & 0_No < y1 - y2 ) by SURREALR:45, SURREALR:46;
A151: 0_No < 1_No - (||.x.|| * y2) by A143, A92, SURREALR:45;
A152: ( 1_No - (||.x.|| * y1) < 0_No & (||.x.|| * y2) - 1_No < 0_No ) by A137, A143, A92, SURREALR:46;
A153: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y1))) + (((y1 - y2) * x1) * (||.x.|| - x2)) by Th29;
A154: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y2))) + (((y2 - y1) * x2) * (x1 - ||.x.||)) by Th29;
A155: ( x2 is positive & x1 is positive ) by A3, A144, A138, Def9;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

proof

A156: ((y2 + (- y1)) * (x1 + (- ||.x.||))) * x2 == ((y2 + (- y1)) * x2) * (x1 + (- ||.x.||)) by SURREALR:69;
0_No < (y2 + (- y1)) * (x1 + (- ||.x.||)) by A150, A149, SURREALR:72;
then 0_No < ((y2 + (- y1)) * (x1 + (- ||.x.||))) * x2 by A155, SURREALR:72;
then A157: 0_No < ((y2 + (- y1)) * x2) * (x1 + (- ||.x.||)) by A156, SURREALO:4;

per cases ;

suppose x2 < x1 ; :: thesis:

then 0_No < x1 - x2 by SURREALR:45;
then A158: 0_No <= (x1 + (- x2)) * (1_No + (- (||.x.|| * y2))) by A151, SURREALR:72;
( 0_No = 0_No + 0_No & 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- ||.x.||))) ) by A157, A158, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A154, SURREALO:4; :: thesis:

end;

suppose x1 == x2 ; :: thesis:

then ( x1 + (- x2) == x2 - x2 & x2 - x2 == 0_No ) by SURREALR:43, SURREALR:39;
then x1 + (- x2) == 0_No by SURREALO:4;
then ( (x1 + (- x2)) * (1_No + (- (||.x.|| * y2))) == 0_No * (1_No + (- (||.x.|| * y2))) & 0_No * (1_No + (- (||.x.|| * y2))) = 0_No ) by SURREALR:51;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- ||.x.||))) by A157, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A154, SURREALO:4; :: thesis:

end;

suppose x1 < x2 ; :: thesis:

then x1 - x2 < 0_No by SURREALR:46;
then A159: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y1))) by A152, SURREALR:72;
0_No < (y1 + (- y2)) * x1 by A150, A155, SURREALR:72;
then 0_No <= ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) by A149, SURREALR:72;
then ( 0_No = 0_No + 0_No & 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) ) by A159, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A153, SURREALO:4; :: thesis:

end;

hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) ; :: thesis:

end;

then (1_No + ((x1 - ||.x.||) * y1)) * x2 < (1_No + ((x2 - ||.x.||) * y2)) * x1 by SURREALR:45;
then (1_No + ((x1 - ||.x.||) * y1)) * Ix1 < (1_No + ((x2 - ||.x.||) * y2)) * Ix2 by A145, A139, A141, A147, Th28;
hence not r <= l by A138, A144, A142, A148, Def13; :: thesis:

end;

suppose r in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider y2 being object such that
A160: ( y2 in (divR (||.x.||,(No_inverses_on ||.x.||))) . N2 & r in divs (y2,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider y2 = y2 as Surreal by A7, A160, A99;
consider x2 being object such that
A161: ( x2 in R_ ||.x.|| & x2 <> 0_No & r = (1_No +' ((x2 +' (-' ||.x.||)) *' y2)) *' ((No_inverses_on ||.x.||) . x2) ) by A160, Def2;
reconsider x2 = x2 as Surreal by A161, SURREAL0:def 16;
A162: ( x2 is positive & x2 in R_ x ) by A3, Def9, A161;
then ( 0_No < x2 & x2 in (L_ x) \/ (R_ x) ) by XBOOLE_0:def 3;
then A163: born x2 in born x by SURREALO:1;
then reconsider Ix2 = inv x2 as Surreal by A162, A3, A2;
A164: x2 * Ix2 == 1_No by A3, A2, A163, A162;
x2 in (L_ ||.x.||) \/ (R_ ||.x.||) by A161, XBOOLE_0:def 3;
then A165: x2 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A161, ZFMISC_1:56;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

proof

( L_ ||.x.|| << {||.x.||} & {||.x.||} << R_ ||.x.|| & ||.x.|| in {||.x.||} ) by TARSKI:def 1, SURREALO:11;
then A166: ( x1 - ||.x.|| < 0_No & 0_No < ||.x.|| - x1 & ||.x.|| - x2 < 0_No & 0_No < x2 - ||.x.|| ) by A138, A161, SURREALR:45, SURREALR:46;
L_ ||.x.|| << R_ ||.x.|| by SURREAL0:45;
then A167: x1 - x2 < 0_No by A161, A138, SURREALR:46;
A168: ( 1_No - (||.x.|| * y1) < 0_No & 1_No - (||.x.|| * y2) < 0_No ) by A137, A160, A92, SURREALR:46;
A169: ((1_No + ((x2 - ||.x.||) * y2)) * x1) + (- ((1_No + ((x1 - ||.x.||) * y1)) * x2)) == ((x1 - x2) * (1_No - (||.x.|| * y1))) + (((y1 - y2) * x1) * (||.x.|| - x2)) by Th29;
A170: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y2))) + (((y2 - y1) * x2) * (x1 - ||.x.||)) by Th29;
A171: ( x2 is positive & x1 is positive ) by A3, A161, A138, Def9;
A172: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y1))) by A167, A168, SURREALR:72;
A173: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y2))) by A167, A168, SURREALR:72;

per cases ;

suppose y1 == y2 ; :: thesis:

then ( y1 + (- y2) == y2 - y2 & y2 - y2 == 0_No ) by SURREALR:43, SURREALR:39;
then y1 + (- y2) == 0_No by SURREALO:4;
then ( (y1 + (- y2)) * x1 == 0_No * x1 & 0_No * x1 = 0_No ) by SURREALR:51;
then ( ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) == 0_No * (||.x.|| + (- x2)) & 0_No * (||.x.|| + (- x2)) = 0_No ) by SURREALR:51;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) by A172, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A169, SURREALO:4; :: thesis:

end;

suppose y1 < y2 ; :: thesis:

then y1 - y2 < 0_No by SURREALR:46;
then (y1 + (- y2)) * x1 < 0_No by A171, SURREALR:74;
then 0_No <= ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) by A166, SURREALR:72;
then ( 0_No = 0_No + 0_No & 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) ) by A172, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A169, SURREALO:4; :: thesis:

end;

suppose y2 < y1 ; :: thesis:

then y2 - y1 < 0_No by SURREALR:46;
then (y2 + (- y1)) * x2 < 0_No by A171, SURREALR:74;
then 0_No <= ((y2 + (- y1)) * x2) * (x1 + (- ||.x.||)) by A166, SURREALR:72;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- ||.x.||))) by A173, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A170, SURREALO:4; :: thesis:

end;

then (1_No + ((x1 - ||.x.||) * y1)) * x2 < (1_No + ((x2 - ||.x.||) * y2)) * x1 by SURREALR:45;
then (1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1 < (1_No + ((x2 + (- ||.x.||)) * y2)) * Ix2 by A162, A139, A141, A164, Th28;
hence not r <= l by A138, A161, A142, A165, Def13; :: thesis:

end;

reconsider UL = Union (divL (||.x.||,(No_inverses_on ||.x.||))), UR = Union (divR (||.x.||,(No_inverses_on ||.x.||))) as surreal-membered set by A5, Th10;
consider M being Ordinal such that
A174: for o being object st o in UL \/ UR holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
A175: inv x = [UL,UR] by A3, Th26;
inv x in Day M by A175, A174, A94, SURREAL0:46;
hence inv x is surreal ; :: thesis:
let y be Surreal; :: thesis:
assume A176: y = inv x ; :: thesis:
set xy = ||.x.|| * y;
A177: ||.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 SURREALR:50;
A178: ( UL = L_ y & L_ y << {y} & {y} << R_ y & R_ y = UR & y in {y} ) by SURREALO:11, A175, A176, TARSKI:def 1;
A179: ( dom (divL (||.x.||,(No_inverses_on ||.x.||))) = NAT & NAT = dom (divR (||.x.||,(No_inverses_on ||.x.||))) ) by Def5, Def6;
A180: {1_No} << R_ (||.x.|| * y)

proof

let r, l be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A181: ( r in {1_No} & l in R_ (||.x.|| * y) ) ; :: thesis:

per cases by A177, A181, XBOOLE_0:def 3;

suppose l in comp ((L_ ||.x.||),||.x.||,y,(R_ y)) ; :: thesis:

then consider x1, y1 being Surreal such that
A182: ( l = ((x1 * y) +' (||.x.|| * y1)) +' (-' (x1 * y1)) & x1 in L_ ||.x.|| & y1 in R_ y ) by SURREALR:def 14;
consider n being Nat such that
A183: ( y1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . n & ( for m being Nat st y1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . m holds
n <= m ) ) by A182, A175, A176, Th27, A179;

per cases ;

suppose x1 = 0_No ; :: thesis:

then A184: l = (0_No + (||.x.|| * y1)) + 0_No by SURREALR:23, A182;
1_No < ||.x.|| * y1 by A183, A92;
hence not l <= r by A184, A181, TARSKI:def 1; :: thesis:

end;

suppose A185: x1 <> 0_No ; :: thesis:

x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A182, XBOOLE_0:def 3;
then A186: ( born x1 in born ||.x.|| & born ||.x.|| c= born x ) by A3, SURREALO:1, Th22;
A187: x1 is positive by A3, A185, A182, Def9;
then reconsider Ix1 = inv x1 as Surreal by A3, A2, A186;
x1 * Ix1 == 1_No by A3, A2, A186, A187;
then A188: ((x1 * y) + (||.x.|| * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - ||.x.||) * y1)) * Ix1))) by Th30;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A182, XBOOLE_0:def 3;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A185, ZFMISC_1:56;
then Ix1 = (No_inverses_on ||.x.||) . x1 by Def13;
then (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' Ix1 in divs (y1,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) by A185, A182, Def2;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) by A183, Def3;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in (((divL (||.x.||,(No_inverses_on ||.x.||))) . n) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)))) \/ (divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then A189: (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . (n + 1) by Th6;
(1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in UL by A179, A189, CARD_5:2;
then 0_No < y - ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1) by A178, SURREALR:45;
then 0_No < x1 * (y + (- ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1))) by A187, SURREALR:72;
then 1_No + 0_No < 1_No + (x1 * (y + (- ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1)))) by SURREALR:44;
then ( 1_No = 1_No + 0_No & 1_No + 0_No < l ) by A182, A188, SURREALO:4;
hence not l <= r by A181, TARSKI:def 1; :: thesis:

end;

suppose l in comp ((R_ ||.x.||),||.x.||,y,(L_ y)) ; :: thesis:

end;

A197: L_ (||.x.|| * y) << {1_No}

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A198: ( l in L_ (||.x.|| * y) & r in {1_No} ) ; :: thesis:

per cases by A177, A198, XBOOLE_0:def 3;

suppose l in comp ((L_ ||.x.||),||.x.||,y,(L_ y)) ; :: thesis:

then consider x1, y1 being Surreal such that
A199: ( l = ((x1 * y) +' (||.x.|| * y1)) +' (-' (x1 * y1)) & x1 in L_ ||.x.|| & y1 in L_ y ) by SURREALR:def 14;
consider n being Nat such that
A200: ( y1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . n & ( for m being Nat st y1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . m holds
n <= m ) ) by A199, A175, A176, Th27, A179;

per cases ;

suppose x1 = 0_No ; :: thesis:

then A201: l = (0_No + (||.x.|| * y1)) + 0_No by SURREALR:23, A199;
||.x.|| * y1 < 1_No by A92, A200;
hence not r <= l by A201, A198, TARSKI:def 1; :: thesis:

end;

suppose A202: x1 <> 0_No ; :: thesis:

end;

suppose l in comp ((R_ ||.x.||),||.x.||,y,(R_ y)) ; :: thesis:

end;

A214: (R_ 1_No) \/ (R_ (||.x.|| * y)) = R_ (||.x.|| * y) ;
reconsider oxy = [((L_ 1_No) \/ (L_ (||.x.|| * y))),(R_ (||.x.|| * y))] as Surreal by A180, A197, A214, SURREALO:14;
A215: 0_No in L_ ||.x.|| by A3, Def9;
0_No in {0_No} by TARSKI:def 1;
then 0_No in {0_No} \/ (divset (UL,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then 0_No in ({0_No} \/ (divset (UL,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)))) \/ (divset (UR,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then A216: 0_No in L_ y by A176, A175, Th12;
((0_No * y) + (||.x.|| * 0_No)) + (- (0_No * 0_No)) = 0_No ;
then 0_No in comp ((L_ ||.x.||),||.x.||,y,(L_ y)) by A216, A215, SURREALR:def 14;
then 0_No in (comp ((L_ ||.x.||),||.x.||,y,(L_ y))) \/ (comp ((R_ ||.x.||),||.x.||,y,(R_ y))) by XBOOLE_0:def 3;
then ||.x.|| * y = oxy by A177, ZFMISC_1:40;
then A217: ||.x.|| * y == 1_No by A180, A197, A214, SURREALO:15;
x * y == ||.x.|| * y by A3, Th18, SURREALR:51;
hence x * y == 1_No by A217, SURREALO:4; :: thesis:

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence for x being Surreal st x is positive holds
( inv x is surreal & ( for y being Surreal st y = inv x holds
x * y == 1_No ) ) ; :: thesis: