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

per cases by A1, XBOOLE_0:def 3;

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

consider y', z' being Element of REAL+ such that
A5: y = y' and
A6: z = z' and
A7: + y,z = y' + z' by A3, A4, Def2;
consider x', yz' being Element of REAL+ such that
A8: x = x' and
A9: + y,z = yz' and
A10: + x,(+ y,z) = x' + yz' by A2, A7, Def2;
consider x'', y'' being Element of REAL+ such that
A11: x = x'' and
A12: y = y'' and
A13: + x,y = x'' + y'' by A2, A3, Def2;
consider xy'', z'' being Element of REAL+ such that
A14: + x,y = xy'' and
A15: z = z'' and
A16: + (+ x,y),z = xy'' + z'' by A4, A13, Def2;
thus + x,(+ y,z) = + (+ x,y),z by A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, ARYTM_2:7; :: thesis:

end;

suppose that A17: x in REAL+ and
A18: y in REAL+ and
A19: z in [:{0 },REAL+ :] ; :: thesis:

consider y', z' being Element of REAL+ such that
A20: y = y' and
A21: z = [0 ,z'] and
A22: + y,z = y' - z' by A18, A19, Def2;
consider x'', y'' being Element of REAL+ such that
A23: x = x'' and
A24: y = y'' and
A25: + x,y = x'' + y'' by A17, A18, Def2;
consider xy'', z'' being Element of REAL+ such that
A26: + x,y = xy'' and
A27: z = [0 ,z''] and
A28: + (+ x,y),z = xy'' - z'' by A19, A25, Def2;
A29: z' = z'' by A21, A27, ZFMISC_1:33;

now

per cases ;

suppose A30: z' <=' y' ; :: thesis:

then A31: + y,z = y' -' z' by A22, ARYTM_1:def 2;
then consider x', yz' being Element of REAL+ such that
A32: x = x' and
A33: + y,z = yz' and
A34: + x,(+ y,z) = x' + yz' by A17, Def2;
thus + x,(+ y,z) = + (+ x,y),z by A20, A23, A24, A25, A26, A28, A29, A30, A31, A32, A33, A34, ARYTM_1:20; :: thesis:

end;

suppose A35: not z' <=' y' ; :: thesis:

then A36: + y,z = [0 ,(z' -' y')] by A22, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A37: x = x' and
A38: + y,z = [0 ,yz'] and
A39: + x,(+ y,z) = x' - yz' by A17, Def2;
thus + x,(+ y,z) = x' - (z' -' y') by A36, A38, A39, ZFMISC_1:33
.= + (+ x,y),z by A20, A23, A24, A25, A26, A28, A29, A35, A37, ARYTM_1:21 ; :: thesis:

end;

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

end;

suppose that A40: x in REAL+ and
A41: y in [:{0 },REAL+ :] and
A42: z in REAL+ ; :: thesis:

consider z', y' being Element of REAL+ such that
A43: z = z' and
A44: y = [0 ,y'] and
A45: + y,z = z' - y' by A41, A42, Def2;
consider x'', y'' being Element of REAL+ such that
A46: x = x'' and
A47: y = [0 ,y''] and
A48: + x,y = x'' - y'' by A40, A41, Def2;
A49: y' = y'' by A44, A47, ZFMISC_1:33;

now

per cases ;

suppose that A50: y' <=' x'' and
A51: y' <=' z' ; :: thesis:

A52: + y,z = z' -' y' by A45, A51, ARYTM_1:def 2;
then consider x', yz' being Element of REAL+ such that
A53: x = x' and
A54: + y,z = yz' and
A55: + x,(+ y,z) = x' + yz' by A40, Def2;
A56: + x,y = x' -' y' by A46, A48, A49, A50, A53, ARYTM_1:def 2;
then consider z'', xy'' being Element of REAL+ such that
A57: z = z'' and
A58: + x,y = xy'' and
A59: + z,(+ x,y) = z'' + xy'' by A42, Def2;
thus + x,(+ y,z) = + (+ x,y),z by A43, A46, A50, A51, A52, A53, A54, A55, A56, A57, A58, A59, ARYTM_1:12; :: thesis:

end;

suppose that A60: y' <=' x'' and
A61: not y' <=' z' ; :: thesis:

A62: + y,z = [0 ,(y' -' z')] by A45, A61, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A63: x = x' and
A64: + y,z = [0 ,yz'] and
A65: + x,(+ y,z) = x' - yz' by A40, Def2;
A66: + x,y = x'' -' y' by A48, A49, A60, ARYTM_1:def 2;
then consider z'', xy'' being Element of REAL+ such that
A67: z = z'' and
A68: + x,y = xy'' and
A69: + z,(+ x,y) = z'' + xy'' by A42, Def2;
thus + x,(+ y,z) = x' - (y' -' z') by A62, A64, A65, ZFMISC_1:33
.= + (+ x,y),z by A43, A46, A60, A61, A63, A66, A67, A68, A69, ARYTM_1:22 ; :: thesis:

end;

suppose that A70: not y' <=' x'' and
A71: y' <=' z' ; :: thesis:

A72: + y,x = [0 ,(y' -' x'')] by A48, A49, A70, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider z'', yx'' being Element of REAL+ such that
A73: z = z'' and
A74: + y,x = [0 ,yx''] and
A75: + z,(+ y,x) = z'' - yx'' by A42, Def2;
A76: + z,y = z' -' y' by A45, A71, ARYTM_1:def 2;
then consider x', zy'' being Element of REAL+ such that
A77: x = x' and
A78: + z,y = zy'' and
A79: + x,(+ z,y) = x' + zy'' by A40, Def2;
thus + x,(+ y,z) = z'' - (y' -' x'') by A43, A46, A70, A71, A73, A76, A77, A78, A79, ARYTM_1:22
.= + (+ x,y),z by A72, A74, A75, ZFMISC_1:33 ; :: thesis:

end;

suppose that A80: not y' <=' x'' and
A81: not y' <=' z' ; :: thesis:

A82: + y,x = [0 ,(y' -' x'')] by A48, A49, A80, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider z'', yx'' being Element of REAL+ such that
A83: z = z'' and
A84: + y,x = [0 ,yx''] and
A85: + z,(+ y,x) = z'' - yx'' by A42, Def2;
A86: + y,z = [0 ,(y' -' z')] by A45, A81, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A87: x = x' and
A88: + y,z = [0 ,yz'] and
A89: + x,(+ y,z) = x' - yz' by A40, Def2;
thus + x,(+ y,z) = x' - (y' -' z') by A86, A88, A89, ZFMISC_1:33
.= z'' - (y' -' x'') by A43, A46, A80, A81, A83, A87, ARYTM_1:23
.= + (+ x,y),z by A82, A84, A85, ZFMISC_1:33 ; :: thesis:

end;

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

end;

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

( ( not z in REAL+ or not y in REAL+ ) & ( not z in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not z in [:{0 },REAL+ :] ) ) by A91, A92, Th5, XBOOLE_0:3;
then consider y', z' being Element of REAL+ such that
A93: y = [0 ,y'] and
A94: z = [0 ,z'] and
A95: + y,z = [0 ,(y' + z')] by Def2;
consider x'', y'' being Element of REAL+ such that
A96: x = x'' and
A97: y = [0 ,y''] and
A98: + x,y = x'' - y'' by A90, A91, Def2;
+ y,z in [:{0 },REAL+ :] by A95, Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A99: x = x' and
A100: + y,z = [0 ,yz'] and
A101: + x,(+ y,z) = x' - yz' by A90, Def2;
A102: y' = y'' by A93, A97, ZFMISC_1:33;

now

per cases ;

suppose A103: y'' <=' x'' ; :: thesis:

then A104: + x,y = x'' -' y'' by A98, ARYTM_1:def 2;
then consider xy'', z'' being Element of REAL+ such that
A105: + x,y = xy'' and
A106: z = [0 ,z''] and
A107: + (+ x,y),z = xy'' - z'' by A92, Def2;
A108: z' = z'' by A94, A106, ZFMISC_1:33;
thus + x,(+ y,z) = x' - (y' + z') by A95, A100, A101, ZFMISC_1:33
.= + (+ x,y),z by A96, A99, A102, A103, A104, A105, A107, A108, ARYTM_1:24 ; :: thesis:

end;

suppose A109: not y'' <=' x'' ; :: thesis:

then A110: + x,y = [0 ,(y'' -' x'')] by A98, ARYTM_1:def 2;
then + x,y in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( ( not z in REAL+ or not + x,y in REAL+ ) & ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) & ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) ) by A92, Th5, XBOOLE_0:3;
then consider xy'', z'' being Element of REAL+ such that
A111: + x,y = [0 ,xy''] and
A112: z = [0 ,z''] and
A113: + (+ x,y),z = [0 ,(xy'' + z'')] by Def2;
A114: z' = z'' by A94, A112, ZFMISC_1:33;
A115: yz' = z' + y' by A95, A100, ZFMISC_1:33;
then y'' <=' yz' by A102, ARYTM_2:20;
then not yz' <=' x' by A96, A99, A109, ARYTM_1:3;
hence + x,(+ y,z) = [0 ,((z' + y') -' x')] by A101, A115, ARYTM_1:def 2
.= [0 ,(z'' + (y'' -' x''))] by A96, A99, A102, A109, A114, ARYTM_1:13
.= + (+ x,y),z by A110, A111, A113, ZFMISC_1:33 ;
:: thesis:

end;

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

end;

suppose that A116: z in REAL+ and
A117: y in REAL+ and
A118: x in [:{0 },REAL+ :] ; :: thesis:

consider y', x' being Element of REAL+ such that
A119: y = y' and
A120: x = [0 ,x'] and
A121: + y,x = y' - x' by A117, A118, Def2;
consider z'', y'' being Element of REAL+ such that
A122: z = z'' and
A123: y = y'' and
A124: + z,y = z'' + y'' by A116, A117, Def2;
consider zy'', x'' being Element of REAL+ such that
A125: + z,y = zy'' and
A126: x = [0 ,x''] and
A127: + (+ z,y),x = zy'' - x'' by A118, A124, Def2;
A128: x' = x'' by A120, A126, ZFMISC_1:33;

now

per cases ;

suppose A129: x' <=' y' ; :: thesis:

then A130: + y,x = y' -' x' by A121, ARYTM_1:def 2;
then consider z', yx' being Element of REAL+ such that
A131: z = z' and
A132: + y,x = yx' and
A133: + z,(+ y,x) = z' + yx' by A116, Def2;
thus + z,(+ y,x) = + (+ z,y),x by A119, A122, A123, A124, A125, A127, A128, A129, A130, A131, A132, A133, ARYTM_1:20; :: thesis:

end;

suppose A134: not x' <=' y' ; :: thesis:

then A135: + y,x = [0 ,(x' -' y')] by A121, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider z', yx' being Element of REAL+ such that
A136: z = z' and
A137: + y,x = [0 ,yx'] and
A138: + z,(+ y,x) = z' - yx' by A116, Def2;
thus + z,(+ y,x) = z' - (x' -' y') by A135, A137, A138, ZFMISC_1:33
.= + (+ z,y),x by A119, A122, A123, A124, A125, A127, A128, A134, A136, ARYTM_1:21 ; :: thesis:

end;

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

end;

suppose that A139: x in [:{0 },REAL+ :] and
A140: y in REAL+ and
A141: z in [:{0 },REAL+ :] ; :: thesis:

consider y', z' being Element of REAL+ such that
A142: y = y' and
A143: z = [0 ,z'] and
A144: + y,z = y' - z' by A140, A141, Def2;
consider x'', y'' being Element of REAL+ such that
A145: x = [0 ,x''] and
A146: y = y'' and
A147: + x,y = y'' - x'' by A139, A140, Def2;

now

per cases ;

suppose that A148: x'' <=' y'' and
A149: z' <=' y' ; :: thesis:

A150: + y,z = y' -' z' by A144, A149, ARYTM_1:def 2;
then consider x', yz' being Element of REAL+ such that
A151: x = [0 ,x'] and
A152: + y,z = yz' and
A153: + x,(+ y,z) = yz' - x' by A139, Def2;
A154: x' = x'' by A145, A151, ZFMISC_1:33;
then A155: + x,y = y' -' x' by A142, A146, A147, A148, ARYTM_1:def 2;
then consider z'', xy'' being Element of REAL+ such that
A156: z = [0 ,z''] and
A157: + x,y = xy'' and
A158: + z,(+ x,y) = xy'' - z'' by A141, Def2;
z' = z'' by A143, A156, ZFMISC_1:33;
hence + x,(+ y,z) = + (+ x,y),z by A142, A146, A148, A149, A150, A152, A153, A154, A155, A157, A158, ARYTM_1:25; :: thesis:

end;

suppose that A159: not x'' <=' y'' and
A160: z' <=' y' ; :: thesis:

A161: + y,z = y' -' z' by A144, A160, ARYTM_1:def 2;
then consider x', yz' being Element of REAL+ such that
A162: x = [0 ,x'] and
A163: + y,z = yz' and
A164: + x,(+ y,z) = yz' - x' by A139, Def2;
A165: x' = x'' by A145, A162, ZFMISC_1:33;
A166: + y,x = [0 ,(x'' -' y'')] by A147, A159, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( ( not z in REAL+ or not + x,y in REAL+ ) & ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) & ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) ) by A141, Th5, XBOOLE_0:3;
then consider z'', yx' being Element of REAL+ such that
A167: z = [0 ,z''] and
A168: + y,x = [0 ,yx'] and
A169: + z,(+ y,x) = [0 ,(z'' + yx')] by Def2;
A170: z' = z'' by A143, A167, ZFMISC_1:33;
yz' <=' y' by A161, A163, ARYTM_1:11;
then not x' <=' yz' by A142, A146, A159, A165, ARYTM_1:3;
hence + x,(+ y,z) = [0 ,(x' -' (y' -' z'))] by A161, A163, A164, ARYTM_1:def 2
.= [0 ,((x'' -' y'') + z'')] by A142, A146, A159, A160, A165, A170, ARYTM_1:14
.= + (+ x,y),z by A166, A168, A169, ZFMISC_1:33 ;
:: thesis:

end;

suppose that A171: not z' <=' y' and
A172: x'' <=' y'' ; :: thesis:

A173: + y,x = y'' -' x'' by A147, A172, ARYTM_1:def 2;
then consider z'', yx'' being Element of REAL+ such that
A174: z = [0 ,z''] and
A175: + y,x = yx'' and
A176: + z,(+ y,x) = yx'' - z'' by A141, Def2;
A177: z'' = z' by A143, A174, ZFMISC_1:33;
A178: + y,z = [0 ,(z' -' y')] by A144, A171, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( ( not x in REAL+ or not + z,y in REAL+ ) & ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) & ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) ) by A139, Th5, XBOOLE_0:3;
then consider x', yz'' being Element of REAL+ such that
A179: x = [0 ,x'] and
A180: + y,z = [0 ,yz''] and
A181: + x,(+ y,z) = [0 ,(x' + yz'')] by Def2;
A182: x'' = x' by A145, A179, ZFMISC_1:33;
yx'' <=' y'' by A173, A175, ARYTM_1:11;
then A183: not z'' <=' yx'' by A142, A146, A171, A177, ARYTM_1:3;
thus + x,(+ y,z) = [0 ,((z' -' y') + x')] by A178, A180, A181, ZFMISC_1:33
.= [0 ,(z'' -' (y'' -' x''))] by A142, A146, A171, A172, A177, A182, ARYTM_1:14
.= + (+ x,y),z by A173, A175, A176, A183, ARYTM_1:def 2 ; :: thesis:

end;

suppose that A184: not x'' <=' y'' and
A185: not z' <=' y' ; :: thesis:

A186: + y,z = [0 ,(z' -' y')] by A144, A185, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( ( not x in REAL+ or not + z,y in REAL+ ) & ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) & ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) ) by A139, Th5, XBOOLE_0:3;
then consider x', yz'' being Element of REAL+ such that
A187: x = [0 ,x'] and
A188: + y,z = [0 ,yz''] and
A189: + x,(+ y,z) = [0 ,(x' + yz'')] by Def2;
A190: + y,x = [0 ,(x'' -' y'')] by A147, A184, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( ( not z in REAL+ or not + x,y in REAL+ ) & ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) & ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) ) by A141, Th5, XBOOLE_0:3;
then consider z'', yx' being Element of REAL+ such that
A191: z = [0 ,z''] and
A192: + y,x = [0 ,yx'] and
A193: + z,(+ y,x) = [0 ,(z'' + yx')] by Def2;
A194: z' = z'' by A143, A191, ZFMISC_1:33;
A195: x' = x'' by A145, A187, ZFMISC_1:33;
thus + x,(+ y,z) = [0 ,((z' -' y') + x')] by A186, A188, A189, ZFMISC_1:33
.= [0 ,((x'' -' y'') + z'')] by A142, A146, A184, A185, A194, A195, ARYTM_1:15
.= + (+ x,y),z by A190, A192, A193, ZFMISC_1:33 ; :: thesis:

end;

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

end;

suppose that A196: z in REAL+ and
A197: y in [:{0 },REAL+ :] and
A198: x in [:{0 },REAL+ :] ; :: thesis:

( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] ) ) by A197, A198, Th5, XBOOLE_0:3;
then consider y', x' being Element of REAL+ such that
A199: y = [0 ,y'] and
A200: x = [0 ,x'] and
A201: + y,x = [0 ,(y' + x')] by Def2;
consider z'', y'' being Element of REAL+ such that
A202: z = z'' and
A203: y = [0 ,y''] and
A204: + z,y = z'' - y'' by A196, A197, Def2;
+ y,x in [:{0 },REAL+ :] by A201, Lm1, ZFMISC_1:106;
then consider z', yx' being Element of REAL+ such that
A205: z = z' and
A206: + y,x = [0 ,yx'] and
A207: + z,(+ y,x) = z' - yx' by A196, Def2;
A208: y' = y'' by A199, A203, ZFMISC_1:33;

now

per cases ;

suppose A209: y'' <=' z'' ; :: thesis:

then A210: + z,y = z'' -' y'' by A204, ARYTM_1:def 2;
then consider zy'', x'' being Element of REAL+ such that
A211: + z,y = zy'' and
A212: x = [0 ,x''] and
A213: + (+ z,y),x = zy'' - x'' by A198, Def2;
A214: x' = x'' by A200, A212, ZFMISC_1:33;
thus + z,(+ y,x) = z' - (y' + x') by A201, A206, A207, ZFMISC_1:33
.= + (+ z,y),x by A202, A205, A208, A209, A210, A211, A213, A214, ARYTM_1:24 ; :: thesis:

end;

suppose A215: not y'' <=' z'' ; :: thesis:

then A216: + z,y = [0 ,(y'' -' z'')] by A204, ARYTM_1:def 2;
then + z,y in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( ( not x in REAL+ or not + z,y in REAL+ ) & ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) & ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) ) by A198, Th5, XBOOLE_0:3;
then consider zy'', x'' being Element of REAL+ such that
A217: + z,y = [0 ,zy''] and
A218: x = [0 ,x''] and
A219: + (+ z,y),x = [0 ,(zy'' + x'')] by Def2;
A220: x' = x'' by A200, A218, ZFMISC_1:33;
A221: yx' = x' + y' by A201, A206, ZFMISC_1:33;
then y'' <=' yx' by A208, ARYTM_2:20;
then not yx' <=' z' by A202, A205, A215, ARYTM_1:3;
hence + z,(+ y,x) = [0 ,((x' + y') -' z')] by A207, A221, ARYTM_1:def 2
.= [0 ,(x'' + (y'' -' z''))] by A202, A205, A208, A215, A220, ARYTM_1:13
.= + (+ z,y),x by A216, A217, A219, ZFMISC_1:33 ;
:: thesis:

end;

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

end;

suppose that A222: x in [:{0 },REAL+ :] and
A223: y in [:{0 },REAL+ :] and
A224: z in [:{0 },REAL+ :] ; :: thesis:

( ( not z in REAL+ or not y in REAL+ ) & ( not z in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not z in [:{0 },REAL+ :] ) ) by A223, A224, Th5, XBOOLE_0:3;
then consider y', z' being Element of REAL+ such that
A225: y = [0 ,y'] and
A226: z = [0 ,z'] and
A227: + y,z = [0 ,(y' + z')] by Def2;
( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] ) ) by A222, A223, Th5, XBOOLE_0:3;
then consider x'', y'' being Element of REAL+ such that
A228: x = [0 ,x''] and
A229: y = [0 ,y''] and
A230: + x,y = [0 ,(x'' + y'')] by Def2;
+ z,y in [:{0 },REAL+ :] by A227, Lm1, ZFMISC_1:106;
then ( ( not x in REAL+ or not + z,y in REAL+ ) & ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) & ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) ) by A222, Th5, XBOOLE_0:3;
then consider x', yz' being Element of REAL+ such that
A231: x = [0 ,x'] and
A232: + y,z = [0 ,yz'] and
A233: + x,(+ y,z) = [0 ,(x' + yz')] by Def2;
+ x,y in [:{0 },REAL+ :] by A230, Lm1, ZFMISC_1:106;
then ( ( not z in REAL+ or not + x,y in REAL+ ) & ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) & ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) ) by A224, Th5, XBOOLE_0:3;
then consider xy'', z'' being Element of REAL+ such that
A234: + x,y = [0 ,xy''] and
A235: z = [0 ,z''] and
A236: + (+ x,y),z = [0 ,(xy'' + z'')] by Def2;
A237: z' = z'' by A226, A235, ZFMISC_1:33;
A238: x' = x'' by A228, A231, ZFMISC_1:33;
A239: y' = y'' by A225, A229, ZFMISC_1:33;
thus + x,(+ y,z) = [0 ,((z' + y') + x')] by A227, A232, A233, ZFMISC_1:33
.= [0 ,(z'' + (y'' + x''))] by A237, A238, A239, ARYTM_2:7
.= + (+ x,y),z by A230, A234, A236, ZFMISC_1:33 ; :: thesis:

end;