let x be Surreal; :: thesis: x - x == 0_No
set y = 0_No ;
defpred S₁[ Ordinal] means for x being Surreal st born x = $1 holds
x + (- x) == 0_No ;
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
let x be Surreal; :: thesis: ( born x = D implies x + (- x) == 0_No )
assume A3: born x = D ; :: thesis: x + (- x) == 0_No
set X = x + (- x);
A4: - x = [(-- (R_ x)),(-- (L_ x))] by Th7;
then ( L_ (- x) = -- (R_ x) & R_ (- x) = -- (L_ x) ) ;
then A5: x + (- x) = [(((L_ x) ++ {(- x)}) \/ ({x} ++ (-- (R_ x)))),(((R_ x) ++ {(- x)}) \/ ({x} ++ (-- (L_ x))))] by Th28;
A6: L_ (x + (- x)) << {0_No}

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in L_ (x + (- x)) or not r in {0_No} or not r <= l )
assume A7: ( l in L_ (x + (- x)) & r in {0_No} & r <= l ) ; :: thesis: contradiction
A8: r = 0_No by A7, TARSKI:def 1;
A9: {r} << R_ l by A7, SURREAL0:43;

per cases ( l in {x} ++ (-- (R_ x)) or l in (L_ x) ++ {(- x)} ) by A5, A7, XBOOLE_0:def 3;

suppose l in {x} ++ (-- (R_ x)) ; :: thesis: contradiction

then consider ll, lr being Surreal such that
A10: ( ll in {x} & lr in -- (R_ x) & l = ll + lr ) by Def8;
consider xr being Surreal such that
A11: ( xr in R_ x & - xr = lr ) by A10, Def4;
x = ll by A10, TARSKI:def 1;
then A12: l = [(((L_ x) ++ {(- xr)}) \/ ({x} ++ (L_ (- xr)))),(((R_ x) ++ {(- xr)}) \/ ({x} ++ (R_ (- xr))))] by Th28, A10, A11;
xr in (L_ x) \/ (R_ x) by A11, XBOOLE_0:def 3;
then A13: xr + (- xr) == 0_No by A3, A2, SURREALO:1;
- xr in {(- xr)} by TARSKI:def 1;
then xr + (- xr) in (R_ x) ++ {(- xr)} by A11, Def8;
then xr + (- xr) in R_ l by A12, XBOOLE_0:def 3;
hence contradiction by A13, A9, A7, A8; :: thesis: verum

end;

suppose l in (L_ x) ++ {(- x)} ; :: thesis: contradiction

then consider xl, lr being Surreal such that
A14: ( xl in L_ x & lr in {(- x)} & l = xl + lr ) by Def8;
lr = - x by A14, TARSKI:def 1;
then A15: l = [(((L_ xl) ++ {(- x)}) \/ ({xl} ++ (L_ (- x)))),(((R_ xl) ++ {(- x)}) \/ ({xl} ++ (R_ (- x))))] by A14, Th28;
xl in (L_ x) \/ (R_ x) by A14, XBOOLE_0:def 3;
then A16: xl + (- xl) == 0_No by A3, A2, SURREALO:1;
( - xl in -- (L_ x) & xl in {xl} ) by A14, Def4, TARSKI:def 1;
then xl + (- xl) in {xl} ++ (-- (L_ x)) by Def8;
then xl + (- xl) in R_ l by A4, A15, XBOOLE_0:def 3;
hence contradiction by A16, A9, A7, A8; :: thesis: verum

end;

end;

end;

{(x + (- x))} << R_ 0_No ;
hence x + (- x) <= 0_No by A6, SURREAL0:43; :: according to SURREALO:def 2 :: thesis: 0_No <= x + (- x)
A17: {0_No} << R_ (x + (- x))

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {0_No} or not r in R_ (x + (- x)) or not r <= l )
assume A18: ( l in {0_No} & r in R_ (x + (- x)) & r <= l ) ; :: thesis: contradiction
A19: l = 0_No by A18, TARSKI:def 1;
A20: L_ r << {l} by SURREAL0:43, A18;

per cases ( r in (R_ x) ++ {(- x)} or r in {x} ++ (-- (L_ x)) ) by A5, A18, XBOOLE_0:def 3;

suppose r in (R_ x) ++ {(- x)} ; :: thesis: contradiction

then consider ll, lr being Surreal such that
A21: ( ll in R_ x & lr in {(- x)} & r = ll + lr ) by Def8;
lr = - x by A21, TARSKI:def 1;
then A22: r = [(((L_ ll) ++ {(- x)}) \/ ({ll} ++ (L_ (- x)))),(((R_ ll) ++ {(- x)}) \/ ({ll} ++ (R_ (- x))))] by A21, Th28;
ll in (L_ x) \/ (R_ x) by A21, XBOOLE_0:def 3;
then A23: ll + (- ll) == 0_No by A3, A2, SURREALO:1;
( - ll in L_ (- x) & ll in {ll} ) by A21, Def4, A4, TARSKI:def 1;
then ll + (- ll) in {ll} ++ (L_ (- x)) by Def8;
then ll + (- ll) in L_ r by A22, XBOOLE_0:def 3;
hence contradiction by A23, A20, A19, A18; :: thesis: verum

end;

suppose r in {x} ++ (-- (L_ x)) ; :: thesis: contradiction

then consider ll, lr being Surreal such that
A24: ( ll in {x} & lr in -- (L_ x) & r = ll + lr ) by Def8;
consider xr being Surreal such that
A25: ( xr in L_ x & - xr = lr ) by A24, Def4;
x = ll by A24, TARSKI:def 1;
then A26: r = [(((L_ x) ++ {(- xr)}) \/ ({x} ++ (L_ (- xr)))),(((R_ x) ++ {(- xr)}) \/ ({x} ++ (R_ (- xr))))] by Th28, A24, A25;
xr in (L_ x) \/ (R_ x) by A25, XBOOLE_0:def 3;
then A27: xr + (- xr) == 0_No by A3, A2, SURREALO:1;
- xr in {(- xr)} by TARSKI:def 1;
then xr + (- xr) in (L_ x) ++ {(- xr)} by A25, Def8;
then xr + (- xr) in L_ r by A26, XBOOLE_0:def 3;
hence contradiction by A27, A20, A18, A19; :: thesis: verum

end;

end;

end;

L_ 0_No << {(x + (- x))} ;
hence 0_No <= x + (- x) by SURREAL0:43, A17; :: thesis: verum

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence x - x == 0_No ; :: thesis: verum