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

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
A3: 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 = {y} ) or ( Y c= (L_ y) \/ (R_ y) & X = {x} ) ) holds
-- (X ++ Y) = (-- X) ++ (-- Y)

proof

let x, y be Surreal; :: thesis: ( (born x) (+) (born y) c= D implies for X, Y being surreal-membered set st ( ( X c= (L_ x) \/ (R_ x) & Y = {y} ) or ( Y c= (L_ y) \/ (R_ y) & X = {x} ) ) holds
-- (X ++ Y) = (-- X) ++ (-- Y) )
assume A4: (born x) (+) (born y) c= D ; :: thesis: for X, Y being surreal-membered set st ( ( X c= (L_ x) \/ (R_ x) & Y = {y} ) or ( Y c= (L_ y) \/ (R_ y) & X = {x} ) ) holds
-- (X ++ Y) = (-- X) ++ (-- Y)
let X, Y be surreal-membered set ; :: thesis: ( ( ( X c= (L_ x) \/ (R_ x) & Y = {y} ) or ( Y c= (L_ y) \/ (R_ y) & X = {x} ) ) implies -- (X ++ Y) = (-- X) ++ (-- Y) )
assume A5: ( ( X c= (L_ x) \/ (R_ x) & Y = {y} ) or ( Y c= (L_ y) \/ (R_ y) & X = {x} ) ) ; :: thesis: -- (X ++ Y) = (-- X) ++ (-- Y)
thus -- (X ++ Y) c= (-- X) ++ (-- Y) :: according to XBOOLE_0:def 10 :: thesis: (-- X) ++ (-- Y) c= -- (X ++ Y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in -- (X ++ Y) or a in (-- X) ++ (-- Y) )
assume a in -- (X ++ Y) ; :: thesis: a in (-- X) ++ (-- Y)
then consider z being Surreal such that
A6: ( z in X ++ Y & a = - z ) by Def4;
consider x1, y1 being Surreal such that
A7: ( x1 in X & y1 in Y & z = x1 + y1 ) by A6, Def8;
( ( born x1 in born x & born y1 = born y ) or ( born x1 = born x & born y1 in born y ) ) by SURREALO:1, A5, A7, TARSKI:def 1;
then (born x1) (+) (born y1) in (born x) (+) (born y) by ORDINAL7:94;
then A8: a = (- x1) + (- y1) by A2, A4, A6, A7;
( - x1 in -- X & - y1 in -- Y ) by A7, Def4;
hence a in (-- X) ++ (-- Y) by A8, Def8; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (-- X) ++ (-- Y) or a in -- (X ++ Y) )
assume a in (-- X) ++ (-- Y) ; :: thesis: a in -- (X ++ Y)
then consider x2, y2 being Surreal such that
A9: ( x2 in -- X & y2 in -- Y & a = x2 + y2 ) by Def8;
consider x1 being Surreal such that
A10: ( x1 in X & x2 = - x1 ) by A9, Def4;
consider y1 being Surreal such that
A11: ( y1 in Y & y2 = - y1 ) by A9, Def4;
A12: x1 + y1 in X ++ Y by A10, A11, Def8;
( ( born x1 in born x & born y1 = born y ) or ( born x1 = born x & born y1 in born y ) ) by SURREALO:1, A5, A10, A11, TARSKI:def 1;
then (born x1) (+) (born y1) in (born x) (+) (born y) by ORDINAL7:94;
then - (x1 + y1) = a by A2, A4, A10, A11, A9;
hence a in -- (X ++ Y) by A12, Def4; :: thesis: verum

end;

let x, y be Surreal; :: thesis: ( (born x) (+) (born y) c= D implies - (x + y) = (- x) + (- y) )
assume A13: (born x) (+) (born y) c= D ; :: thesis: - (x + y) = (- x) + (- y)
A14: L_ x c= (L_ x) \/ (R_ x) by XBOOLE_1:7;
A15: R_ x c= (L_ x) \/ (R_ x) by XBOOLE_1:7;
A16: L_ y c= (L_ y) \/ (R_ y) by XBOOLE_1:7;
A17: R_ y c= (L_ y) \/ (R_ y) by XBOOLE_1:7;
A18: x + y = [(((L_ x) ++ {y}) \/ ({x} ++ (L_ y))),(((R_ x) ++ {y}) \/ ({x} ++ (R_ y)))] by Th28;
A19: ( L_ (- x) = -- (R_ x) & R_ (- x) = -- (L_ x) & (- y) `1 = -- (R_ y) & (- y) `2 = -- (L_ y) ) by Th8;
A20: ( {(- x)} = -- {x} & {(- y)} = -- {y} ) by Th21;
A21: (R_ (- x)) ++ {(- y)} = -- ((L_ x) ++ {y}) by A19, A20, A14, A3, A13;
A22: {(- x)} ++ (R_ (- y)) = -- ({x} ++ (L_ y)) by A19, A20, A16, A3, A13;
A23: (L_ (- x)) ++ {(- y)} = -- ((R_ x) ++ {y}) by A19, A20, A15, A3, A13;
{(- x)} ++ (L_ (- y)) = -- ({x} ++ (R_ y)) by A19, A20, A17, A3, A13;
then A24: ((L_ (- x)) ++ {(- y)}) \/ ({(- x)} ++ (L_ (- y))) = -- (((R_ x) ++ {y}) \/ ({x} ++ (R_ y))) by A23, Th20;
thus (- x) + (- y) = [(((L_ (- x)) ++ {(- y)}) \/ ({(- x)} ++ (L_ (- y)))),(((R_ (- x)) ++ {(- y)}) \/ ({(- x)} ++ (R_ (- y))))] by Th28
.= [(-- (R_ (x + y))),(-- (L_ (x + y)))] by A18, A22, A21, Th20, A24
.= - (x + y) by Th7 ; :: thesis: verum

end;

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