let x, y, z be Element of REAL ; :: thesis:

hence * x,(+ y,z) = 0 by Th14
.= + o,o by Th13
.= + (* x,y),o by A1, Th14
.= + (* x,y),(* x,z) by A1, Th14 ;
:: thesis:

end;

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

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

end;

suppose that A20: ( x in REAL+ & x <> 0 ) and
A21: y in REAL+ and
A22: z in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

consider x', y' being Element of REAL+ such that
A23: x = x' and
A24: y = y' and
A25: * x,y = x' *' y' by A20, A21, Def3;
consider x'', z' being Element of REAL+ such that
A26: x = x'' and
A27: z = [0 ,z'] and
A28: * x,z = [0 ,(x'' *' z')] by A20, A22, Def3;
consider y'', z'' being Element of REAL+ such that
A29: y = y'' and
A30: z = [0 ,z''] and
A31: + y,z = y'' - z'' by A21, A22, Def2;
A32: z' = z'' by A27, A30, ZFMISC_1:33;
* x,z in [:{0 },REAL+ :] by A28, Lm1, ZFMISC_1:106;
then consider xy', xz' being Element of REAL+ such that
A33: * x,y = xy' and
A34: * x,z = [0 ,xz'] and
A35: + (* x,y),(* x,z) = xy' - xz' by A25, Def2;

now

per cases ;

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

then A37: + y,z = y'' -' z'' by A31, ARYTM_1:def 2;
then consider x''', yz' being Element of REAL+ such that
A38: x = x''' and
A39: + y,z = yz' and
A40: * x,(+ y,z) = x''' *' yz' by A20, Def3;
thus * x,(+ y,z) = (x' *' y') - (x'' *' z') by A23, A24, A26, A29, A32, A36, A37, A38, A39, A40, ARYTM_1:26
.= + (* x,y),(* x,z) by A25, A28, A33, A34, A35, ZFMISC_1:33 ; :: thesis:

end;

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

then A42: + y,z = [0 ,(z'' -' y'')] by A31, 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
A43: x = x''' and
A44: + y,z = [0 ,yz'] and
A45: * x,(+ y,z) = [0 ,(x''' *' yz')] by A20, Def3;
thus * x,(+ y,z) = [0 ,(x''' *' (z'' -' y''))] by A42, A44, A45, ZFMISC_1:33
.= (x' *' y') - (x'' *' z') by A20, A23, A24, A26, A29, A32, A41, A43, ARYTM_1:27
.= + (* x,y),(* x,z) by A25, A28, A33, A34, A35, ZFMISC_1:33 ; :: thesis:

end;

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

end;

suppose that A46: ( x in REAL+ & x <> 0 ) and
A47: z in REAL+ and
A48: y in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

consider x', z' being Element of REAL+ such that
A49: x = x' and
A50: z = z' and
A51: * x,z = x' *' z' by A46, A47, Def3;
consider x'', y' being Element of REAL+ such that
A52: x = x'' and
A53: y = [0 ,y'] and
A54: * x,y = [0 ,(x'' *' y')] by A46, A48, Def3;
consider z'', y'' being Element of REAL+ such that
A55: z = z'' and
A56: y = [0 ,y''] and
A57: + z,y = z'' - y'' by A47, A48, Def2;
A58: y' = y'' by A53, A56, ZFMISC_1:33;
* x,y in [:{0 },REAL+ :] by A54, Lm1, ZFMISC_1:106;
then consider xz', xy' being Element of REAL+ such that
A59: * x,z = xz' and
A60: * x,y = [0 ,xy'] and
A61: + (* x,z),(* x,y) = xz' - xy' by A51, Def2;

now

per cases ;

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

then A63: + z,y = z'' -' y'' by A57, ARYTM_1:def 2;
then consider x''', zy' being Element of REAL+ such that
A64: x = x''' and
A65: + z,y = zy' and
A66: * x,(+ z,y) = x''' *' zy' by A46, Def3;
thus * x,(+ z,y) = (x' *' z') - (x'' *' y') by A49, A50, A52, A55, A58, A62, A63, A64, A65, A66, ARYTM_1:26
.= + (* x,z),(* x,y) by A51, A54, A59, A60, A61, ZFMISC_1:33 ; :: thesis:

end;

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

then A68: + z,y = [0 ,(y'' -' z'')] by A57, ARYTM_1:def 2;
then + z,y in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x''', zy' being Element of REAL+ such that
A69: x = x''' and
A70: + z,y = [0 ,zy'] and
A71: * x,(+ z,y) = [0 ,(x''' *' zy')] by A46, Def3;
thus * x,(+ z,y) = [0 ,(x''' *' (y'' -' z''))] by A68, A70, A71, ZFMISC_1:33
.= (x' *' z') - (x'' *' y') by A46, A49, A50, A52, A55, A58, A67, A69, ARYTM_1:27
.= + (* x,z),(* x,y) by A51, A54, A59, A60, A61, ZFMISC_1:33 ; :: thesis:

end;

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

end;

suppose that A72: ( x in REAL+ & x <> 0 ) and
A73: y in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A74: z in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

consider x', y' being Element of REAL+ such that
A75: x = x' and
A76: y = [0 ,y'] and
A77: * x,y = [0 ,(x' *' y')] by A72, A73, Def3;
consider x'', z' being Element of REAL+ such that
A78: x = x'' and
A79: z = [0 ,z'] and
A80: * x,z = [0 ,(x'' *' z')] by A72, A74, Def3;
( * x,y in [:{0 },REAL+ :] & * x,z in [:{0 },REAL+ :] ) by A77, A80, Lm1, ZFMISC_1:106;
then ( ( not * x,y in REAL+ or not * x,z in REAL+ ) & ( not * x,y in REAL+ or not * x,z in [:{0 },REAL+ :] ) & ( not * x,y in [:{0 },REAL+ :] or not * x,z in REAL+ ) ) by Th5, XBOOLE_0:3;
then consider xy', xz' being Element of REAL+ such that
A81: * x,y = [0 ,xy'] and
A82: * x,z = [0 ,xz'] and
A83: + (* x,y),(* x,z) = [0 ,(xy' + xz')] by Def2;
( ( not y in REAL+ or not z in REAL+ ) & ( not y in REAL+ or not z in [:{0 },REAL+ :] ) & ( not y in [:{0 },REAL+ :] or not z in REAL+ ) ) by A73, A74, Th5, XBOOLE_0:3;
then consider y'', z'' being Element of REAL+ such that
A84: y = [0 ,y''] and
A85: z = [0 ,z''] and
A86: + y,z = [0 ,(y'' + z'')] by Def2;
+ y,z in [:{0 },REAL+ :] by A86, 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) = [0 ,(x''' *' yz')] by A72, Def3;
A90: xy' = x' *' y' by A77, A81, ZFMISC_1:33;
A91: y' = y'' by A76, A84, ZFMISC_1:33;
A92: z' = z'' by A79, A85, ZFMISC_1:33;
thus * x,(+ y,z) = [0 ,(x''' *' (y'' + z''))] by A86, A88, A89, ZFMISC_1:33
.= [0 ,((x' *' y') + (x' *' z'))] by A75, A87, A91, A92, ARYTM_2:14
.= + (* x,y),(* x,z) by A75, A78, A80, A82, A83, A90, ZFMISC_1:33 ; :: thesis:

end;

suppose that A93: x in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A94: y in REAL+ and
A95: z in REAL+ ; :: thesis:

consider y'', z'' being Element of REAL+ such that
A96: y = y'' and
A97: z = z'' and
A98: + y,z = y'' + z'' by A94, A95, Def2;

now

per cases ;

suppose that A99: y <> 0 and
A100: z <> 0 ; :: thesis:

consider x', y' being Element of REAL+ such that
A101: x = [0 ,x'] and
A102: y = y' and
A103: * x,y = [0 ,(y' *' x')] by A93, A94, A99, Def3;
consider x'', z' being Element of REAL+ such that
A104: x = [0 ,x''] and
A105: z = z' and
A106: * x,z = [0 ,(z' *' x'')] by A93, A95, A100, Def3;
( * x,y in [:{0 },REAL+ :] & * x,z in [:{0 },REAL+ :] ) by A103, A106, Lm1, ZFMISC_1:106;
then ( ( not * x,y in REAL+ or not * x,z in REAL+ ) & ( not * x,y in REAL+ or not * x,z in [:{0 },REAL+ :] ) & ( not * x,y in [:{0 },REAL+ :] or not * x,z in REAL+ ) ) by Th5, XBOOLE_0:3;
then consider xy', xz' being Element of REAL+ such that
A107: * x,y = [0 ,xy'] and
A108: * x,z = [0 ,xz'] and
A109: + (* x,y),(* x,z) = [0 ,(xy' + xz')] by Def2;
y'' + z'' <> 0 by A97, A100, ARYTM_2:6;
then consider x''', yz' being Element of REAL+ such that
A110: x = [0 ,x'''] and
A111: + y,z = yz' and
A112: * x,(+ y,z) = [0 ,(yz' *' x''')] by A93, A98, Def3;
A113: xy' = x' *' y' by A103, A107, ZFMISC_1:33;
A114: x' = x'' by A101, A104, ZFMISC_1:33;
x'' = x''' by A104, A110, ZFMISC_1:33;
hence * x,(+ y,z) = [0 ,((x' *' y') + (x'' *' z'))] by A96, A97, A98, A102, A105, A111, A112, A114, ARYTM_2:14
.= + (* x,y),(* x,z) by A106, A108, A109, A113, ZFMISC_1:33 ;
:: thesis:

end;

suppose A115: x = 0 ; :: thesis:

hence * x,(+ y,z) = 0 by Th14
.= + o,o by Th13
.= + (* x,y),o by A115, Th14
.= + (* x,y),(* x,z) by A115, Th14 ;
:: thesis:

end;

suppose A116: z = 0 ; :: thesis:

hence * x,(+ y,z) = * x,y by Th13
.= + (* x,y),(* x,z) by A116, Th13, Th14 ;
:: thesis:

end;

suppose A117: y = 0 ; :: thesis:

hence * x,(+ y,z) = * x,z by Th13
.= + (* x,y),(* x,z) by A117, Th13, Th14 ;
:: thesis:

end;

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

end;

suppose that A118: x in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A119: y in REAL+ and
A120: z in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

consider x'', z' being Element of REAL+ such that
A121: x = [0 ,x''] and
A122: z = [0 ,z'] and
A123: * x,z = z' *' x'' by A118, A120, Def3;

now

per cases ;

suppose y <> 0 ; :: thesis:

then consider x', y' being Element of REAL+ such that
A124: x = [0 ,x'] and
A125: y = y' and
A126: * x,y = [0 ,(y' *' x')] by A118, A119, Def3;
consider y'', z'' being Element of REAL+ such that
A127: y = y'' and
A128: z = [0 ,z''] and
A129: + y,z = y'' - z'' by A120, A125, Def2;
* x,y in [:{0 },REAL+ :] by A126, Lm1, ZFMISC_1:106;
then consider xy', xz' being Element of REAL+ such that
A130: * x,y = [0 ,xy'] and
A131: * x,z = xz' and
A132: + (* x,y),(* x,z) = xz' - xy' by A123, Def2;
A133: z' = z'' by A122, A128, ZFMISC_1:33;

now

per cases ;

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

then A135: + y,z = y'' -' z'' by A129, ARYTM_1:def 2;

now

per cases ;

suppose A136: + y,z <> 0 ; :: thesis:

then consider x''', yz' being Element of REAL+ such that
A137: x = [0 ,x'''] and
A138: + y,z = yz' and
A139: * x,(+ y,z) = [0 ,(yz' *' x''')] by A118, A135, Def3;
A140: x' = x'' by A121, A124, ZFMISC_1:33;
A141: x'' = x''' by A121, A137, ZFMISC_1:33;
A142: z' = z'' by A122, A128, ZFMISC_1:33;
not x in {[0 ,0 ]} by NUMBERS:def 1, XBOOLE_0:def 5;
then x''' <> 0 by A137, TARSKI:def 1;
hence * x,(+ y,z) = (x' *' z') - (x' *' y') by A125, A127, A134, A135, A136, A138, A139, A140, A141, A142, ARYTM_1:28
.= + (* x,y),(* x,z) by A123, A126, A130, A131, A132, A140, ZFMISC_1:33 ;
:: thesis:

end;

suppose A143: + y,z = 0 ; :: thesis:

then A144: y'' = z'' by A134, A135, ARYTM_1:10;
A145: xy' = x' *' y' by A126, A130, ZFMISC_1:33;
A146: x' = x'' by A121, A124, ZFMISC_1:33;
thus * x,(+ y,z) = 0 by A143, Th14
.= + (* x,y),(* x,z) by A123, A125, A127, A131, A132, A133, A144, A145, A146, ARYTM_1:18 ; :: thesis:

end;

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

end;

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

then A148: + y,z = [0 ,(z'' -' y'')] by A129, 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
A149: x = [0 ,x'''] and
A150: + y,z = [0 ,yz'] and
A151: * x,(+ y,z) = yz' *' x''' by A118, Def3;
A152: x' = x'' by A121, A124, ZFMISC_1:33;
A153: x'' = x''' by A121, A149, ZFMISC_1:33;
thus * x,(+ y,z) = x''' *' (z'' -' y'') by A148, A150, A151, ZFMISC_1:33
.= (x'' *' z') - (x' *' y') by A125, A127, A133, A147, A152, A153, ARYTM_1:26
.= + (* x,y),(* x,z) by A123, A126, A130, A131, A132, ZFMISC_1:33 ; :: thesis:

end;

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

end;

suppose A154: y = 0 ; :: thesis:

hence * x,(+ y,z) = * x,z by Th13
.= + (* x,y),(* x,z) by A154, Th13, Th14 ;
:: thesis:

end;

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

end;

suppose that A155: x in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A156: z in REAL+ and
A157: y in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

consider x'', y' being Element of REAL+ such that
A158: x = [0 ,x''] and
A159: y = [0 ,y'] and
A160: * x,y = y' *' x'' by A155, A157, Def3;

now

per cases ;

suppose z <> 0 ; :: thesis:

then consider x', z' being Element of REAL+ such that
A161: x = [0 ,x'] and
A162: z = z' and
A163: * x,z = [0 ,(z' *' x')] by A155, A156, Def3;
consider z'', y'' being Element of REAL+ such that
A164: z = z'' and
A165: y = [0 ,y''] and
A166: + z,y = z'' - y'' by A157, A162, Def2;
* x,z in [:{0 },REAL+ :] by A163, Lm1, ZFMISC_1:106;
then consider xz', xy' being Element of REAL+ such that
A167: * x,z = [0 ,xz'] and
A168: * x,y = xy' and
A169: + (* x,z),(* x,y) = xy' - xz' by A160, Def2;
A170: y' = y'' by A159, A165, ZFMISC_1:33;

now

per cases ;

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

then A172: + z,y = z'' -' y'' by A166, ARYTM_1:def 2;

now

per cases ;

suppose A173: + z,y <> 0 ; :: thesis:

then consider x''', zy' being Element of REAL+ such that
A174: x = [0 ,x'''] and
A175: + z,y = zy' and
A176: * x,(+ z,y) = [0 ,(zy' *' x''')] by A155, A172, Def3;
A177: x' = x'' by A158, A161, ZFMISC_1:33;
A178: x'' = x''' by A158, A174, ZFMISC_1:33;
A179: y' = y'' by A159, A165, ZFMISC_1:33;
not x in {[0 ,0 ]} by NUMBERS:def 1, XBOOLE_0:def 5;
then x''' <> 0 by A174, TARSKI:def 1;
hence * x,(+ z,y) = (x' *' y') - (x' *' z') by A162, A164, A171, A172, A173, A175, A176, A177, A178, A179, ARYTM_1:28
.= + (* x,z),(* x,y) by A160, A163, A167, A168, A169, A177, ZFMISC_1:33 ;
:: thesis:

end;

suppose A180: + z,y = 0 ; :: thesis:

then A181: z'' = y'' by A171, A172, ARYTM_1:10;
A182: xz' = x' *' z' by A163, A167, ZFMISC_1:33;
A183: x' = x'' by A158, A161, ZFMISC_1:33;
thus * x,(+ z,y) = 0 by A180, Th14
.= + (* x,z),(* x,y) by A160, A162, A164, A168, A169, A170, A181, A182, A183, ARYTM_1:18 ; :: thesis:

end;

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

end;

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

then A185: + z,y = [0 ,(y'' -' z'')] by A166, ARYTM_1:def 2;
then + z,y in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x''', zy' being Element of REAL+ such that
A186: x = [0 ,x'''] and
A187: + z,y = [0 ,zy'] and
A188: * x,(+ z,y) = zy' *' x''' by A155, Def3;
A189: x' = x'' by A158, A161, ZFMISC_1:33;
A190: x'' = x''' by A158, A186, ZFMISC_1:33;
thus * x,(+ y,z) = x''' *' (y'' -' z'') by A185, A187, A188, ZFMISC_1:33
.= (x'' *' y') - (x' *' z') by A162, A164, A170, A184, A189, A190, ARYTM_1:26
.= + (* x,y),(* x,z) by A160, A163, A167, A168, A169, ZFMISC_1:33 ; :: thesis:

end;

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

end;

suppose A191: z = 0 ; :: thesis:

hence * x,(+ y,z) = * x,y by Th13
.= + (* x,y),(* x,z) by A191, Th13, Th14 ;
:: thesis:

end;

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

end;

suppose that A192: x in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A193: y in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A194: z in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

consider x', y' being Element of REAL+ such that
A195: x = [0 ,x'] and
A196: y = [0 ,y'] and
A197: * x,y = y' *' x' by A192, A193, Def3;
consider x'', z' being Element of REAL+ such that
A198: x = [0 ,x''] and
A199: z = [0 ,z'] and
A200: * x,z = z' *' x'' by A192, A194, Def3;
consider xy', xz' being Element of REAL+ such that
A201: * x,y = xy' and
A202: * x,z = xz' and
A203: + (* x,y),(* x,z) = xy' + xz' by A197, A200, Def2;
( ( not y in REAL+ or not z in REAL+ ) & ( not y in REAL+ or not z in [:{0 },REAL+ :] ) & ( not y in [:{0 },REAL+ :] or not z in REAL+ ) ) by A193, A194, Th5, XBOOLE_0:3;
then consider y'', z'' being Element of REAL+ such that
A204: y = [0 ,y''] and
A205: z = [0 ,z''] and
A206: + y,z = [0 ,(y'' + z'')] by Def2;
+ y,z in [:{0 },REAL+ :] by A206, Lm1, ZFMISC_1:106;
then consider x''', yz' being Element of REAL+ such that
A207: x = [0 ,x'''] and
A208: + y,z = [0 ,yz'] and
A209: * x,(+ y,z) = yz' *' x''' by A192, Def3;
A210: x' = x'' by A195, A198, ZFMISC_1:33;
A211: x' = x''' by A195, A207, ZFMISC_1:33;
A212: y' = y'' by A196, A204, ZFMISC_1:33;
A213: z' = z'' by A199, A205, ZFMISC_1:33;
thus * x,(+ y,z) = x''' *' (y'' + z'') by A206, A208, A209, ZFMISC_1:33
.= + (* x,y),(* x,z) by A197, A200, A201, A202, A203, A210, A211, A212, A213, ARYTM_2:14 ; :: thesis:

end;

suppose A214: ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not y in REAL+ or not z in REAL+ ) & ( not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not y in REAL+ or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in REAL+ ) & ( not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) ) ; :: thesis:

A215: not [0 ,0 ] in REAL+ by ARYTM_2:3;
REAL = (REAL+ \ {[0 ,0 ]}) \/ ([:{0 },REAL+ :] \ {[0 ,0 ]}) by NUMBERS:def 1, XBOOLE_1:42
.= REAL+ \/ ([:{0 },REAL+ :] \ {[0 ,0 ]}) by A215, ZFMISC_1:65 ;
hence * x,(+ y,z) = + (* x,y),(* x,z) by A214, XBOOLE_0:def 3; :: thesis:

end;