let x, y be Surreal; :: thesis: x + y = y + x
defpred S₁[ Ordinal] means for x, y being Surreal st (born x) (+) (born y) c= $1 holds
x + y = y + x;
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 c= Y ++ X

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 c= Y ++ X )
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 c= Y ++ X
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 c= Y ++ X )
assume A5: ( ( X c= (L_ x) \/ (R_ x) & Y = {y} ) or ( Y c= (L_ y) \/ (R_ y) & X = {x} ) ) ; :: thesis: X ++ Y c= Y ++ X
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X ++ Y or a in Y ++ X )
assume a in X ++ Y ; :: thesis: a in Y ++ X
then consider x1, y1 being Surreal such that
A6: ( x1 in X & y1 in Y & a = x1 + y1 ) by Def8;
( ( born x1 in born x & born y1 = born y ) or ( born x1 = born x & born y1 in born y ) ) by SURREALO:1, A5, A6, TARSKI:def 1;
then (born x1) (+) (born y1) in (born x) (+) (born y) by ORDINAL7:94;
then x1 + y1 = y1 + x1 by A2, A4;
hence a in Y ++ X by A6, Def8; :: thesis: verum

end;

let x, y be Surreal; :: thesis: ( (born x) (+) (born y) c= D implies x + y = y + x )
assume A7: (born x) (+) (born y) c= D ; :: thesis: x + y = y + x
L_ x c= (L_ x) \/ (R_ x) by XBOOLE_1:7;
then ( (L_ x) ++ {y} c= {y} ++ (L_ x) & {y} ++ (L_ x) c= (L_ x) ++ {y} ) by A7, A3;
then A8: (L_ x) ++ {y} = {y} ++ (L_ x) by XBOOLE_0:def 10;
R_ x c= (L_ x) \/ (R_ x) by XBOOLE_1:7;
then ( (R_ x) ++ {y} c= {y} ++ (R_ x) & {y} ++ (R_ x) c= (R_ x) ++ {y} ) by A7, A3;
then A9: (R_ x) ++ {y} = {y} ++ (R_ x) by XBOOLE_0:def 10;
L_ y c= (L_ y) \/ (R_ y) by XBOOLE_1:7;
then ( (L_ y) ++ {x} c= {x} ++ (L_ y) & {x} ++ (L_ y) c= (L_ y) ++ {x} ) by A7, A3;
then A10: (L_ y) ++ {x} = {x} ++ (L_ y) by XBOOLE_0:def 10;
R_ y c= (L_ y) \/ (R_ y) by XBOOLE_1:7;
then A11: ( (R_ y) ++ {x} c= {x} ++ (R_ y) & {x} ++ (R_ y) c= (R_ y) ++ {x} ) by A7, A3;
thus x + y = [(((L_ x) ++ {y}) \/ ({x} ++ (L_ y))),(((R_ x) ++ {y}) \/ ({x} ++ (R_ y)))] by Th28
.= [(({y} ++ (L_ x)) \/ ((L_ y) ++ {x})),(({y} ++ (R_ x)) \/ ((R_ y) ++ {x}))] by A8, A9, A10, A11, XBOOLE_0:def 10
.= y + x by Th28 ; :: thesis: verum

end;

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