let x, y, z be Surreal; :: thesis: for X, Y, Z being surreal-membered set st ( X = L_ x or X = R_ x or X = {x} ) & ( Y = L_ y or Y = R_ y or Y = {y} ) & ( Z = L_ z or Z = R_ z or Z = {z} ) & ( X <> {x} or Y <> {y} or Z <> {z} ) holds
for x1, y1, z1 being Surreal st x1 in X & y1 in Y & z1 in Z holds
((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z)
set D = ((born x) (+) (born y)) (+) (born z);
let X, Y, Z be surreal-membered set ; :: thesis: ( ( X = L_ x or X = R_ x or X = {x} ) & ( Y = L_ y or Y = R_ y or Y = {y} ) & ( Z = L_ z or Z = R_ z or Z = {z} ) & ( X <> {x} or Y <> {y} or Z <> {z} ) implies for x1, y1, z1 being Surreal st x1 in X & y1 in Y & z1 in Z holds
((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) )
assume A1: ( ( X = L_ x or X = R_ x or X = {x} ) & ( Y = L_ y or Y = R_ y or Y = {y} ) & ( Z = L_ z or Z = R_ z or Z = {z} ) & ( X <> {x} or Y <> {y} or Z <> {z} ) ) ; :: thesis: for x1, y1, z1 being Surreal st x1 in X & y1 in Y & z1 in Z holds
((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z)
let x1, y1, z1 be Surreal; :: thesis: ( x1 in X & y1 in Y & z1 in Z implies ((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) )
assume A2: ( x1 in X & y1 in Y & z1 in Z ) ; :: thesis: ((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z)

per cases ( Z <> {z} or Z = {z} ) ;

suppose Z <> {z} ; :: thesis: ((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z)

then A3: z1 in (L_ z) \/ (R_ z) by A1, A2, XBOOLE_0:def 3;
( x1 in (L_ x) \/ (R_ x) or x1 = x ) by A2, A1, TARSKI:def 1, XBOOLE_0:def 3;
then A4: born x1 c= born x by SURREALO:1, ORDINAL1:def 2;
( y1 in (L_ y) \/ (R_ y) or y1 = y ) by A2, A1, TARSKI:def 1, XBOOLE_0:def 3;
then born y1 c= born y by SURREALO:1, ORDINAL1:def 2;
then ( (born x1) (+) (born y1) c= (born x1) (+) (born y) & (born x1) (+) (born y) c= (born x) (+) (born y) ) by A4, ORDINAL7:95;
then (born x1) (+) (born y1) c= (born x) (+) (born y) by XBOOLE_1:1;
then ( ((born x1) (+) (born y1)) (+) (born z1) c= ((born x) (+) (born y)) (+) (born z1) & ((born x) (+) (born y)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) ) by A3, SURREALO:1, ORDINAL7:94, ORDINAL7:95;
hence ((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) by ORDINAL1:12; :: thesis: verum

end;

suppose A5: Z = {z} ; :: thesis: ((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z)

then ( ( x1 in (L_ x) \/ (R_ x) & y1 in (L_ y) \/ (R_ y) ) or ( x1 in (L_ x) \/ (R_ x) & y1 = y ) or ( x1 = x & y1 in (L_ y) \/ (R_ y) ) ) by A1, A2, XBOOLE_0:def 3, TARSKI:def 1;
then ( (born x1) (+) (born y1) in (born x) (+) (born y) or ( (born x1) (+) (born y1) in (born x1) (+) (born y) & (born x1) (+) (born y) in (born x) (+) (born y) ) ) by ORDINAL7:94, SURREALO:1;
then (born x1) (+) (born y1) in (born x) (+) (born y) by ORDINAL1:10;
then ((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z1) by ORDINAL7:94;
hence ((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) by A2, A5, TARSKI:def 1; :: thesis: verum

end;

end;