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

proof

let X, Y, Z be set ; :: thesis: ( ( for x, y, z being Surreal st x in X & y in Y & z in Z holds
((born x) (+) (born y)) (+) (born z) in D ) implies X ++ (Y ++ Z) = (X ++ Y) ++ Z )
assume A4: for x, y, z being Surreal st x in X & y in Y & z in Z holds
((born x) (+) (born y)) (+) (born z) in D ; :: thesis: X ++ (Y ++ Z) = (X ++ Y) ++ Z
thus X ++ (Y ++ Z) c= (X ++ Y) ++ Z :: according to XBOOLE_0:def 10 :: thesis: (X ++ Y) ++ Z c= X ++ (Y ++ Z)

proof

let xyz be object ; :: according to TARSKI:def 3 :: thesis: ( not xyz in X ++ (Y ++ Z) or xyz in (X ++ Y) ++ Z )
assume xyz in X ++ (Y ++ Z) ; :: thesis: xyz in (X ++ Y) ++ Z
then consider x, yz being Surreal such that
A5: ( x in X & yz in Y ++ Z & xyz = x + yz ) by Def8;
consider y, z being Surreal such that
A6: ( y in Y & z in Z & yz = y + z ) by A5, Def8;
x + y in X ++ Y by A5, A6, Def8;
then A7: (x + y) + z in (X ++ Y) ++ Z by A6, Def8;
((born x) (+) (born y)) (+) (born z) in D by A5, A6, A4;
hence xyz in (X ++ Y) ++ Z by A5, A6, A7, A2; :: thesis: verum

end;

let xyz be object ; :: according to TARSKI:def 3 :: thesis: ( not xyz in (X ++ Y) ++ Z or xyz in X ++ (Y ++ Z) )
assume xyz in (X ++ Y) ++ Z ; :: thesis: xyz in X ++ (Y ++ Z)
then consider xy, z being Surreal such that
A8: ( xy in X ++ Y & z in Z & xyz = xy + z ) by Def8;
consider x, y being Surreal such that
A9: ( x in X & y in Y & xy = x + y ) by A8, Def8;
y + z in Y ++ Z by A8, A9, Def8;
then A10: x + (y + z) in X ++ (Y ++ Z) by A9, Def8;
((born x) (+) (born y)) (+) (born z) in D by A8, A9, A4;
hence xyz in X ++ (Y ++ Z) by A8, A9, A10, A2; :: thesis: verum

end;

let x, y, z be Surreal; :: thesis: ( ((born x) (+) (born y)) (+) (born z) c= D implies (x + y) + z = x + (y + z) )
assume A11: ((born x) (+) (born y)) (+) (born z) c= D ; :: thesis: (x + y) + z = x + (y + z)
set xy = x + y;
set yz = y + z;
A12: x + y = [(((L_ x) ++ {y}) \/ ({x} ++ (L_ y))),(((R_ x) ++ {y}) \/ ({x} ++ (R_ y)))] by Th28;
A13: y + z = [(((L_ y) ++ {z}) \/ ({y} ++ (L_ z))),(((R_ y) ++ {z}) \/ ({y} ++ (R_ z)))] by Th28;
A14: for a, b, c being Surreal st a in L_ x & b in {y} & c in {z} holds
((born a) (+) (born b)) (+) (born c) in D

proof

let a, b, c be Surreal; :: thesis: ( a in L_ x & b in {y} & c in {z} implies ((born a) (+) (born b)) (+) (born c) in D )
assume ( a in L_ x & b in {y} & c in {z} ) ; :: thesis: ((born a) (+) (born b)) (+) (born c) in D
then A15: ( a in (L_ x) \/ (R_ x) & b = y & c = z ) by TARSKI:def 1, XBOOLE_0:def 3;
then (born a) (+) (born b) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then ((born a) (+) (born b)) (+) (born c) in ((born x) (+) (born y)) (+) (born z) by ORDINAL7:94, A15;
hence ((born a) (+) (born b)) (+) (born c) in D by A11; :: thesis: verum

end;

A16: for a, b, c being Surreal st a in {x} & b in L_ y & c in {z} holds
((born a) (+) (born b)) (+) (born c) in D

proof

let a, b, c be Surreal; :: thesis: ( a in {x} & b in L_ y & c in {z} implies ((born a) (+) (born b)) (+) (born c) in D )
assume ( a in {x} & b in L_ y & c in {z} ) ; :: thesis: ((born a) (+) (born b)) (+) (born c) in D
then A17: ( a = x & b in (L_ y) \/ (R_ y) & c = z ) by TARSKI:def 1, XBOOLE_0:def 3;
then (born a) (+) (born b) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then ((born a) (+) (born b)) (+) (born c) in ((born x) (+) (born y)) (+) (born z) by ORDINAL7:94, A17;
hence ((born a) (+) (born b)) (+) (born c) in D by A11; :: thesis: verum

end;

A18: for a, b, c being Surreal st a in {x} & b in {y} & c in L_ z holds
((born a) (+) (born b)) (+) (born c) in D

proof

let a, b, c be Surreal; :: thesis: ( a in {x} & b in {y} & c in L_ z implies ((born a) (+) (born b)) (+) (born c) in D )
assume ( a in {x} & b in {y} & c in L_ z ) ; :: thesis: ((born a) (+) (born b)) (+) (born c) in D
then ( a = x & b = y & c in (L_ z) \/ (R_ z) ) by TARSKI:def 1, XBOOLE_0:def 3;
then ((born a) (+) (born b)) (+) (born c) in ((born x) (+) (born y)) (+) (born z) by SURREALO:1, ORDINAL7:94;
hence ((born a) (+) (born b)) (+) (born c) in D by A11; :: thesis: verum

end;

A19: ((((L_ x) ++ {y}) \/ ({x} ++ (L_ y))) ++ {z}) \/ ({(x + y)} ++ (L_ z)) = ((((L_ x) ++ {y}) ++ {z}) \/ (({x} ++ (L_ y)) ++ {z})) \/ ({(x + y)} ++ (L_ z)) by Th33
.= (((L_ x) ++ ({y} ++ {z})) \/ (({x} ++ (L_ y)) ++ {z})) \/ ({(x + y)} ++ (L_ z)) by A14, A3
.= (((L_ x) ++ ({y} ++ {z})) \/ ({x} ++ ((L_ y) ++ {z}))) \/ ({(x + y)} ++ (L_ z)) by A16, A3
.= (((L_ x) ++ ({y} ++ {z})) \/ ({x} ++ ((L_ y) ++ {z}))) \/ (({x} ++ {y}) ++ (L_ z)) by Th36
.= (((L_ x) ++ ({y} ++ {z})) \/ ({x} ++ ((L_ y) ++ {z}))) \/ ({x} ++ ({y} ++ (L_ z))) by A18, A3
.= ((L_ x) ++ ({y} ++ {z})) \/ (({x} ++ ((L_ y) ++ {z})) \/ ({x} ++ ({y} ++ (L_ z)))) by XBOOLE_1:4
.= ((L_ x) ++ ({y} ++ {z})) \/ ({x} ++ (((L_ y) ++ {z}) \/ ({y} ++ (L_ z)))) by Th33
.= ((L_ x) ++ {(y + z)}) \/ ({x} ++ (L_ (y + z))) by A13, Th36 ;
A20: for a, b, c being Surreal st a in R_ x & b in {y} & c in {z} holds
((born a) (+) (born b)) (+) (born c) in D

proof

let a, b, c be Surreal; :: thesis: ( a in R_ x & b in {y} & c in {z} implies ((born a) (+) (born b)) (+) (born c) in D )
assume ( a in R_ x & b in {y} & c in {z} ) ; :: thesis: ((born a) (+) (born b)) (+) (born c) in D
then A21: ( a in (L_ x) \/ (R_ x) & b = y & c = z ) by TARSKI:def 1, XBOOLE_0:def 3;
then (born a) (+) (born b) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then ((born a) (+) (born b)) (+) (born c) in ((born x) (+) (born y)) (+) (born z) by ORDINAL7:94, A21;
hence ((born a) (+) (born b)) (+) (born c) in D by A11; :: thesis: verum

end;

A22: for a, b, c being Surreal st a in {x} & b in R_ y & c in {z} holds
((born a) (+) (born b)) (+) (born c) in D

proof

let a, b, c be Surreal; :: thesis: ( a in {x} & b in R_ y & c in {z} implies ((born a) (+) (born b)) (+) (born c) in D )
assume ( a in {x} & b in R_ y & c in {z} ) ; :: thesis: ((born a) (+) (born b)) (+) (born c) in D
then A23: ( a = x & b in (L_ y) \/ (R_ y) & c = z ) by TARSKI:def 1, XBOOLE_0:def 3;
then (born a) (+) (born b) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then ((born a) (+) (born b)) (+) (born c) in ((born x) (+) (born y)) (+) (born z) by ORDINAL7:94, A23;
hence ((born a) (+) (born b)) (+) (born c) in D by A11; :: thesis: verum

end;

A24: for a, b, c being Surreal st a in {x} & b in {y} & c in R_ z holds
((born a) (+) (born b)) (+) (born c) in D

proof

let a, b, c be Surreal; :: thesis: ( a in {x} & b in {y} & c in R_ z implies ((born a) (+) (born b)) (+) (born c) in D )
assume ( a in {x} & b in {y} & c in R_ z ) ; :: thesis: ((born a) (+) (born b)) (+) (born c) in D
then ( a = x & b = y & c in (L_ z) \/ (R_ z) ) by TARSKI:def 1, XBOOLE_0:def 3;
then ((born a) (+) (born b)) (+) (born c) in ((born x) (+) (born y)) (+) (born z) by SURREALO:1, ORDINAL7:94;
hence ((born a) (+) (born b)) (+) (born c) in D by A11; :: thesis: verum

end;

A25: ((((R_ x) ++ {y}) \/ ({x} ++ (R_ y))) ++ {z}) \/ ({(x + y)} ++ (R_ z)) = ((((R_ x) ++ {y}) ++ {z}) \/ (({x} ++ (R_ y)) ++ {z})) \/ ({(x + y)} ++ (R_ z)) by Th33
.= (((R_ x) ++ ({y} ++ {z})) \/ (({x} ++ (R_ y)) ++ {z})) \/ ({(x + y)} ++ (R_ z)) by A20, A3
.= (((R_ x) ++ {(y + z)}) \/ (({x} ++ (R_ y)) ++ {z})) \/ ({(x + y)} ++ (R_ z)) by Th36
.= (((R_ x) ++ {(y + z)}) \/ (({x} ++ (R_ y)) ++ {z})) \/ (({x} ++ {y}) ++ (R_ z)) by Th36
.= (((R_ x) ++ {(y + z)}) \/ ({x} ++ ((R_ y) ++ {z}))) \/ (({x} ++ {y}) ++ (R_ z)) by A22, A3
.= (((R_ x) ++ {(y + z)}) \/ ({x} ++ ((R_ y) ++ {z}))) \/ ({x} ++ ({y} ++ (R_ z))) by A24, A3
.= ((R_ x) ++ {(y + z)}) \/ (({x} ++ ((R_ y) ++ {z})) \/ ({x} ++ ({y} ++ (R_ z)))) by XBOOLE_1:4
.= ((R_ x) ++ {(y + z)}) \/ ({x} ++ (R_ (y + z))) by A13, Th33 ;
(x + y) + z = [(((L_ (x + y)) ++ {z}) \/ ({(x + y)} ++ (L_ z))),(((R_ (x + y)) ++ {z}) \/ ({(x + y)} ++ (R_ z)))] by Th28
.= [(((L_ x) ++ {(y + z)}) \/ ({x} ++ (L_ (y + z)))),(((R_ x) ++ {(y + z)}) \/ ({x} ++ (R_ (y + z))))] by A25, A19, A12 ;
hence (x + y) + z = x + (y + z) by Th28; :: thesis: verum

end;

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