let x, y, z be Element of REAL ; :: thesis:
A1: ( x in REAL+ \/ [:{0 },REAL+ :] & y in REAL+ \/ [:{0 },REAL+ :] ) by NUMBERS:def 1, XBOOLE_0:def 5;
A2: z in REAL+ \/ [:{0 },REAL+ :] by NUMBERS:def 1, XBOOLE_0:def 5;

per cases by A1, A2, XBOOLE_0:def 3;

suppose that A3: x in REAL+ and
A4: y in REAL+ and
A5: z in REAL+ ; :: thesis:

A6: ex x99, y99 being Element of REAL+ st
( x = x99 & y = y99 & + x,y = x99 + y99 ) by A3, A4, Def2;
then A7: ex xy99, z99 being Element of REAL+ st
( + x,y = xy99 & z = z99 & + (+ x,y),z = xy99 + z99 ) by A5, Def2;
A8: ex y9, z9 being Element of REAL+ st
( y = y9 & z = z9 & + y,z = y9 + z9 ) by A4, A5, Def2;
then ex x9, yz9 being Element of REAL+ st
( x = x9 & + y,z = yz9 & + x,(+ y,z) = x9 + yz9 ) by A3, Def2;
hence + x,(+ y,z) = + (+ x,y),z by A8, A6, A7, ARYTM_2:7; :: thesis:

end;

suppose that A9: x in REAL+ and
A10: y in REAL+ and
A11: z in [:{0 },REAL+ :] ; :: thesis:

A12: ex x99, y99 being Element of REAL+ st
( x = x99 & y = y99 & + x,y = x99 + y99 ) by A9, A10, Def2;
then consider xy99, z99 being Element of REAL+ such that
A13: + x,y = xy99 and
A14: z = [0 ,z99] and
A15: + (+ x,y),z = xy99 - z99 by A11, Def2;
consider y9, z9 being Element of REAL+ such that
A16: y = y9 and
A17: z = [0 ,z9] and
A18: + y,z = y9 - z9 by A10, A11, Def2;
A19: z9 = z99 by A17, A14, ZFMISC_1:33;

now

per cases ;

suppose A20: z9 <=' y9 ; :: thesis:

then A21: + y,z = y9 -' z9 by A18, ARYTM_1:def 2;
then ex x9, yz9 being Element of REAL+ st
( x = x9 & + y,z = yz9 & + x,(+ y,z) = x9 + yz9 ) by A9, Def2;
hence + x,(+ y,z) = + (+ x,y),z by A16, A12, A13, A15, A19, A20, A21, ARYTM_1:20; :: thesis:

end;

suppose A22: not z9 <=' y9 ; :: thesis:

then A23: + y,z = [0 ,(z9 -' y9)] by A18, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x9, yz9 being Element of REAL+ such that
A24: x = x9 and
A25: ( + y,z = [0 ,yz9] & + x,(+ y,z) = x9 - yz9 ) by A9, Def2;
thus + x,(+ y,z) = x9 - (z9 -' y9) by A23, A25, ZFMISC_1:33
.= + (+ x,y),z by A16, A12, A13, A15, A19, A22, A24, ARYTM_1:21 ; :: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A26: x in REAL+ and
A27: y in [:{0 },REAL+ :] and
A28: z in REAL+ ; :: thesis:

consider x99, y99 being Element of REAL+ such that
A29: x = x99 and
A30: y = [0 ,y99] and
A31: + x,y = x99 - y99 by A26, A27, Def2;
consider z9, y9 being Element of REAL+ such that
A32: z = z9 and
A33: y = [0 ,y9] and
A34: + y,z = z9 - y9 by A27, A28, Def2;
A35: y9 = y99 by A33, A30, ZFMISC_1:33;

now

per cases ;

suppose that A36: y9 <=' x99 and
A37: y9 <=' z9 ; :: thesis:

A38: + y,z = z9 -' y9 by A34, A37, ARYTM_1:def 2;
then consider x9, yz9 being Element of REAL+ such that
A39: x = x9 and
A40: ( + y,z = yz9 & + x,(+ y,z) = x9 + yz9 ) by A26, Def2;
A41: + x,y = x9 -' y9 by A29, A31, A35, A36, A39, ARYTM_1:def 2;
then ex z99, xy99 being Element of REAL+ st
( z = z99 & + x,y = xy99 & + z,(+ x,y) = z99 + xy99 ) by A28, Def2;
hence + x,(+ y,z) = + (+ x,y),z by A32, A29, A36, A37, A38, A39, A40, A41, ARYTM_1:12; :: thesis:

end;

suppose that A42: y9 <=' x99 and
A43: not y9 <=' z9 ; :: thesis:

A44: + x,y = x99 -' y9 by A31, A35, A42, ARYTM_1:def 2;
then A45: ex z99, xy99 being Element of REAL+ st
( z = z99 & + x,y = xy99 & + z,(+ x,y) = z99 + xy99 ) by A28, Def2;
A46: + y,z = [0 ,(y9 -' z9)] by A34, A43, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x9, yz9 being Element of REAL+ such that
A47: x = x9 and
A48: ( + y,z = [0 ,yz9] & + x,(+ y,z) = x9 - yz9 ) by A26, Def2;
thus + x,(+ y,z) = x9 - (y9 -' z9) by A46, A48, ZFMISC_1:33
.= + (+ x,y),z by A32, A29, A42, A43, A47, A44, A45, ARYTM_1:22 ; :: thesis:

end;

suppose that A49: not y9 <=' x99 and
A50: y9 <=' z9 ; :: thesis:

A51: + y,x = [0 ,(y9 -' x99)] by A31, A35, A49, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider z99, yx99 being Element of REAL+ such that
A52: z = z99 and
A53: ( + y,x = [0 ,yx99] & + z,(+ y,x) = z99 - yx99 ) by A28, Def2;
A54: + z,y = z9 -' y9 by A34, A50, ARYTM_1:def 2;
then ex x9, zy99 being Element of REAL+ st
( x = x9 & + z,y = zy99 & + x,(+ z,y) = x9 + zy99 ) by A26, Def2;
hence + x,(+ y,z) = z99 - (y9 -' x99) by A32, A29, A49, A50, A52, A54, ARYTM_1:22
.= + (+ x,y),z by A51, A53, ZFMISC_1:33 ;
:: thesis:

end;

suppose that A55: not y9 <=' x99 and
A56: not y9 <=' z9 ; :: thesis:

A57: + y,z = [0 ,(y9 -' z9)] by A34, A56, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x9, yz9 being Element of REAL+ such that
A58: x = x9 and
A59: ( + y,z = [0 ,yz9] & + x,(+ y,z) = x9 - yz9 ) by A26, Def2;
A60: + y,x = [0 ,(y9 -' x99)] by A31, A35, A55, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider z99, yx99 being Element of REAL+ such that
A61: z = z99 and
A62: ( + y,x = [0 ,yx99] & + z,(+ y,x) = z99 - yx99 ) by A28, Def2;
thus + x,(+ y,z) = x9 - (y9 -' z9) by A57, A59, ZFMISC_1:33
.= z99 - (y9 -' x99) by A32, A29, A55, A56, A61, A58, ARYTM_1:23
.= + (+ x,y),z by A60, A62, ZFMISC_1:33 ; :: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A63: x in REAL+ and
A64: y in [:{0 },REAL+ :] and
A65: z in [:{0 },REAL+ :] ; :: thesis:

( ( not z in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not z in [:{0 },REAL+ :] ) ) by A64, A65, Th5, XBOOLE_0:3;
then consider y9, z9 being Element of REAL+ such that
A66: y = [0 ,y9] and
A67: z = [0 ,z9] and
A68: + y,z = [0 ,(y9 + z9)] by A64, Def2;
+ y,z in [:{0 },REAL+ :] by A68, Lm1, ZFMISC_1:106;
then consider x9, yz9 being Element of REAL+ such that
A69: x = x9 and
A70: + y,z = [0 ,yz9] and
A71: + x,(+ y,z) = x9 - yz9 by A63, Def2;
consider x99, y99 being Element of REAL+ such that
A72: x = x99 and
A73: y = [0 ,y99] and
A74: + x,y = x99 - y99 by A63, A64, Def2;
A75: y9 = y99 by A66, A73, ZFMISC_1:33;

now

per cases ;

suppose A76: y99 <=' x99 ; :: thesis:

then A77: + x,y = x99 -' y99 by A74, ARYTM_1:def 2;
then consider xy99, z99 being Element of REAL+ such that
A78: + x,y = xy99 and
A79: z = [0 ,z99] and
A80: + (+ x,y),z = xy99 - z99 by A65, Def2;
A81: z9 = z99 by A67, A79, ZFMISC_1:33;
thus + x,(+ y,z) = x9 - (y9 + z9) by A68, A70, A71, ZFMISC_1:33
.= + (+ x,y),z by A72, A69, A75, A76, A77, A78, A80, A81, ARYTM_1:24 ; :: thesis:

end;

suppose A82: not y99 <=' x99 ; :: thesis:

A83: ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) by A65, Th5, XBOOLE_0:3;
A84: + x,y = [0 ,(y99 -' x99)] by A74, A82, ARYTM_1:def 2;
then + x,y in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider xy99, z99 being Element of REAL+ such that
A85: + x,y = [0 ,xy99] and
A86: z = [0 ,z99] and
A87: + (+ x,y),z = [0 ,(xy99 + z99)] by A84, A83, Def2, Lm1, ZFMISC_1:106;
A88: z9 = z99 by A67, A86, ZFMISC_1:33;
A89: yz9 = z9 + y9 by A68, A70, ZFMISC_1:33;
then y99 <=' yz9 by A75, ARYTM_2:20;
then not yz9 <=' x9 by A72, A69, A82, ARYTM_1:3;
hence + x,(+ y,z) = [0 ,((z9 + y9) -' x9)] by A71, A89, ARYTM_1:def 2
.= [0 ,(z99 + (y99 -' x99))] by A72, A69, A75, A82, A88, ARYTM_1:13
.= + (+ x,y),z by A84, A85, A87, ZFMISC_1:33 ;
:: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A90: z in REAL+ and
A91: y in REAL+ and
A92: x in [:{0 },REAL+ :] ; :: thesis:

A93: ex z99, y99 being Element of REAL+ st
( z = z99 & y = y99 & + z,y = z99 + y99 ) by A90, A91, Def2;
then consider zy99, x99 being Element of REAL+ such that
A94: + z,y = zy99 and
A95: x = [0 ,x99] and
A96: + (+ z,y),x = zy99 - x99 by A92, Def2;
consider y9, x9 being Element of REAL+ such that
A97: y = y9 and
A98: x = [0 ,x9] and
A99: + y,x = y9 - x9 by A91, A92, Def2;
A100: x9 = x99 by A98, A95, ZFMISC_1:33;

now

per cases ;

suppose A101: x9 <=' y9 ; :: thesis:

then A102: + y,x = y9 -' x9 by A99, ARYTM_1:def 2;
then ex z9, yx9 being Element of REAL+ st
( z = z9 & + y,x = yx9 & + z,(+ y,x) = z9 + yx9 ) by A90, Def2;
hence + z,(+ y,x) = + (+ z,y),x by A97, A93, A94, A96, A100, A101, A102, ARYTM_1:20; :: thesis:

end;

suppose A103: not x9 <=' y9 ; :: thesis:

then A104: + y,x = [0 ,(x9 -' y9)] by A99, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider z9, yx9 being Element of REAL+ such that
A105: z = z9 and
A106: ( + y,x = [0 ,yx9] & + z,(+ y,x) = z9 - yx9 ) by A90, Def2;
thus + z,(+ y,x) = z9 - (x9 -' y9) by A104, A106, ZFMISC_1:33
.= + (+ z,y),x by A97, A93, A94, A96, A100, A103, A105, ARYTM_1:21 ; :: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A107: x in [:{0 },REAL+ :] and
A108: y in REAL+ and
A109: z in [:{0 },REAL+ :] ; :: thesis:

consider y9, z9 being Element of REAL+ such that
A110: y = y9 and
A111: z = [0 ,z9] and
A112: + y,z = y9 - z9 by A108, A109, Def2;
consider x99, y99 being Element of REAL+ such that
A113: x = [0 ,x99] and
A114: y = y99 and
A115: + x,y = y99 - x99 by A107, A108, Def2;

now

per cases ;

suppose that A116: x99 <=' y99 and
A117: z9 <=' y9 ; :: thesis:

A118: + y,z = y9 -' z9 by A112, A117, ARYTM_1:def 2;
then consider x9, yz9 being Element of REAL+ such that
A119: x = [0 ,x9] and
A120: ( + y,z = yz9 & + x,(+ y,z) = yz9 - x9 ) by A107, Def2;
A121: x9 = x99 by A113, A119, ZFMISC_1:33;
then A122: + x,y = y9 -' x9 by A110, A114, A115, A116, ARYTM_1:def 2;
then consider z99, xy99 being Element of REAL+ such that
A123: z = [0 ,z99] and
A124: ( + x,y = xy99 & + z,(+ x,y) = xy99 - z99 ) by A109, Def2;
z9 = z99 by A111, A123, ZFMISC_1:33;
hence + x,(+ y,z) = + (+ x,y),z by A110, A114, A116, A117, A118, A120, A121, A122, A124, ARYTM_1:25; :: thesis:

end;

suppose that A125: not x99 <=' y99 and
A126: z9 <=' y9 ; :: thesis:

A127: ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) by A109, Th5, XBOOLE_0:3;
A128: + y,x = [0 ,(x99 -' y99)] by A115, A125, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider z99, yx9 being Element of REAL+ such that
A129: z = [0 ,z99] and
A130: ( + y,x = [0 ,yx9] & + z,(+ y,x) = [0 ,(z99 + yx9)] ) by A128, A127, Def2, Lm1, ZFMISC_1:106;
A131: z9 = z99 by A111, A129, ZFMISC_1:33;
A132: + y,z = y9 -' z9 by A112, A126, ARYTM_1:def 2;
then consider x9, yz9 being Element of REAL+ such that
A133: x = [0 ,x9] and
A134: + y,z = yz9 and
A135: + x,(+ y,z) = yz9 - x9 by A107, Def2;
A136: x9 = x99 by A113, A133, ZFMISC_1:33;
yz9 <=' y9 by A132, A134, ARYTM_1:11;
then not x9 <=' yz9 by A110, A114, A125, A136, ARYTM_1:3;
hence + x,(+ y,z) = [0 ,(x9 -' (y9 -' z9))] by A132, A134, A135, ARYTM_1:def 2
.= [0 ,((x99 -' y99) + z99)] by A110, A114, A125, A126, A136, A131, ARYTM_1:14
.= + (+ x,y),z by A128, A130, ZFMISC_1:33 ;
:: thesis:

end;

suppose that A137: not z9 <=' y9 and
A138: x99 <=' y99 ; :: thesis:

A139: ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) by A107, Th5, XBOOLE_0:3;
A140: + y,z = [0 ,(z9 -' y9)] by A112, A137, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider x9, yz99 being Element of REAL+ such that
A141: x = [0 ,x9] and
A142: ( + y,z = [0 ,yz99] & + x,(+ y,z) = [0 ,(x9 + yz99)] ) by A140, A139, Def2, Lm1, ZFMISC_1:106;
A143: x99 = x9 by A113, A141, ZFMISC_1:33;
A144: + y,x = y99 -' x99 by A115, A138, ARYTM_1:def 2;
then consider z99, yx99 being Element of REAL+ such that
A145: z = [0 ,z99] and
A146: + y,x = yx99 and
A147: + z,(+ y,x) = yx99 - z99 by A109, Def2;
A148: z99 = z9 by A111, A145, ZFMISC_1:33;
yx99 <=' y99 by A144, A146, ARYTM_1:11;
then A149: not z99 <=' yx99 by A110, A114, A137, A148, ARYTM_1:3;
thus + x,(+ y,z) = [0 ,((z9 -' y9) + x9)] by A140, A142, ZFMISC_1:33
.= [0 ,(z99 -' (y99 -' x99))] by A110, A114, A137, A138, A148, A143, ARYTM_1:14
.= + (+ x,y),z by A144, A146, A147, A149, ARYTM_1:def 2 ; :: thesis:

end;

suppose that A150: not x99 <=' y99 and
A151: not z9 <=' y9 ; :: thesis:

A152: ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) by A107, Th5, XBOOLE_0:3;
A153: ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) by A109, Th5, XBOOLE_0:3;
A154: + y,x = [0 ,(x99 -' y99)] by A115, A150, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider z99, yx9 being Element of REAL+ such that
A155: z = [0 ,z99] and
A156: ( + y,x = [0 ,yx9] & + z,(+ y,x) = [0 ,(z99 + yx9)] ) by A154, A153, Def2, Lm1, ZFMISC_1:106;
A157: z9 = z99 by A111, A155, ZFMISC_1:33;
A158: + y,z = [0 ,(z9 -' y9)] by A112, A151, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider x9, yz99 being Element of REAL+ such that
A159: x = [0 ,x9] and
A160: ( + y,z = [0 ,yz99] & + x,(+ y,z) = [0 ,(x9 + yz99)] ) by A158, A152, Def2, Lm1, ZFMISC_1:106;
A161: x9 = x99 by A113, A159, ZFMISC_1:33;
thus + x,(+ y,z) = [0 ,((z9 -' y9) + x9)] by A158, A160, ZFMISC_1:33
.= [0 ,((x99 -' y99) + z99)] by A110, A114, A150, A151, A157, A161, ARYTM_1:15
.= + (+ x,y),z by A154, A156, ZFMISC_1:33 ; :: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A162: z in REAL+ and
A163: y in [:{0 },REAL+ :] and
A164: x in [:{0 },REAL+ :] ; :: thesis:

( ( not x in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] ) ) by A163, A164, Th5, XBOOLE_0:3;
then consider y9, x9 being Element of REAL+ such that
A165: y = [0 ,y9] and
A166: x = [0 ,x9] and
A167: + y,x = [0 ,(y9 + x9)] by A163, Def2;
+ y,x in [:{0 },REAL+ :] by A167, Lm1, ZFMISC_1:106;
then consider z9, yx9 being Element of REAL+ such that
A168: z = z9 and
A169: + y,x = [0 ,yx9] and
A170: + z,(+ y,x) = z9 - yx9 by A162, Def2;
consider z99, y99 being Element of REAL+ such that
A171: z = z99 and
A172: y = [0 ,y99] and
A173: + z,y = z99 - y99 by A162, A163, Def2;
A174: y9 = y99 by A165, A172, ZFMISC_1:33;

now

per cases ;

suppose A175: y99 <=' z99 ; :: thesis:

then A176: + z,y = z99 -' y99 by A173, ARYTM_1:def 2;
then consider zy99, x99 being Element of REAL+ such that
A177: + z,y = zy99 and
A178: x = [0 ,x99] and
A179: + (+ z,y),x = zy99 - x99 by A164, Def2;
A180: x9 = x99 by A166, A178, ZFMISC_1:33;
thus + z,(+ y,x) = z9 - (y9 + x9) by A167, A169, A170, ZFMISC_1:33
.= + (+ z,y),x by A171, A168, A174, A175, A176, A177, A179, A180, ARYTM_1:24 ; :: thesis:

end;

suppose A181: not y99 <=' z99 ; :: thesis:

A182: ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) by A164, Th5, XBOOLE_0:3;
A183: + z,y = [0 ,(y99 -' z99)] by A173, A181, ARYTM_1:def 2;
then + z,y in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider zy99, x99 being Element of REAL+ such that
A184: + z,y = [0 ,zy99] and
A185: x = [0 ,x99] and
A186: + (+ z,y),x = [0 ,(zy99 + x99)] by A183, A182, Def2, Lm1, ZFMISC_1:106;
A187: x9 = x99 by A166, A185, ZFMISC_1:33;
A188: yx9 = x9 + y9 by A167, A169, ZFMISC_1:33;
then y99 <=' yx9 by A174, ARYTM_2:20;
then not yx9 <=' z9 by A171, A168, A181, ARYTM_1:3;
hence + z,(+ y,x) = [0 ,((x9 + y9) -' z9)] by A170, A188, ARYTM_1:def 2
.= [0 ,(x99 + (y99 -' z99))] by A171, A168, A174, A181, A187, ARYTM_1:13
.= + (+ z,y),x by A183, A184, A186, ZFMISC_1:33 ;
:: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A189: x in [:{0 },REAL+ :] and
A190: y in [:{0 },REAL+ :] and
A191: z in [:{0 },REAL+ :] ; :: thesis:

A192: ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) by A189, Th5, XBOOLE_0:3;
( ( not z in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not z in [:{0 },REAL+ :] ) ) by A190, A191, Th5, XBOOLE_0:3;
then consider y9, z9 being Element of REAL+ such that
A193: y = [0 ,y9] and
A194: z = [0 ,z9] and
A195: + y,z = [0 ,(y9 + z9)] by A190, Def2;
+ z,y in [:{0 },REAL+ :] by A195, Lm1, ZFMISC_1:106;
then ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider x9, yz9 being Element of REAL+ such that
A196: x = [0 ,x9] and
A197: ( + y,z = [0 ,yz9] & + x,(+ y,z) = [0 ,(x9 + yz9)] ) by A195, A192, Def2, Lm1, ZFMISC_1:106;
A198: ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) by A191, Th5, XBOOLE_0:3;
( ( not x in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] ) ) by A189, A190, Th5, XBOOLE_0:3;
then consider x99, y99 being Element of REAL+ such that
A199: x = [0 ,x99] and
A200: y = [0 ,y99] and
A201: + x,y = [0 ,(x99 + y99)] by A189, Def2;
A202: x9 = x99 by A199, A196, ZFMISC_1:33;
+ x,y in [:{0 },REAL+ :] by A201, Lm1, ZFMISC_1:106;
then ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider xy99, z99 being Element of REAL+ such that
A203: + x,y = [0 ,xy99] and
A204: z = [0 ,z99] and
A205: + (+ x,y),z = [0 ,(xy99 + z99)] by A201, A198, Def2, Lm1, ZFMISC_1:106;
A206: z9 = z99 by A194, A204, ZFMISC_1:33;
A207: y9 = y99 by A193, A200, ZFMISC_1:33;
thus + x,(+ y,z) = [0 ,((z9 + y9) + x9)] by A195, A197, ZFMISC_1:33
.= [0 ,(z99 + (y99 + x99))] by A206, A202, A207, ARYTM_2:7
.= + (+ x,y),z by A201, A203, A205, ZFMISC_1:33 ; :: thesis:

end;