let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C holds (max f,g) ++ (max f,h) c=
let f, g, h be Membership_Func of C; :: thesis: (max f,g) ++ (max f,h) c=
let c be Element of C; :: according to FUZZY_1:def 3 :: thesis: (max f,(g ++ h)) . c <= ((max f,g) ++ (max f,h)) . c
A1: ((max f,g) ++ (max f,h)) . c = (((max f,g) . c) + ((max f,h) . c)) - (((max f,g) . c) * ((max f,h) . c)) by Def3
.= ((max (f . c),(g . c)) + ((max f,h) . c)) - (((max f,g) . c) * ((max f,h) . c)) by FUZZY_1:6
.= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - (((max f,g) . c) * ((max f,h) . c)) by FUZZY_1:6
.= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * ((max f,h) . c)) by FUZZY_1:6
.= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * (max (f . c),(h . c))) by FUZZY_1:6 ;
A2: max (f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))) <= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * (max (f . c),(h . c)))

proof

per cases ( ( max (f . c),(g . c) = f . c & max (f . c),(h . c) = f . c ) or ( max (f . c),(g . c) = f . c & max (f . c),(h . c) = h . c ) or ( max (f . c),(g . c) = g . c & max (f . c),(h . c) = f . c ) or ( max (f . c),(g . c) = g . c & max (f . c),(h . c) = h . c ) ) by XXREAL_0:16;

suppose A3: ( max (f . c),(g . c) = f . c & max (f . c),(h . c) = f . c ) ; :: thesis: max (f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))) <= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * (max (f . c),(h . c)))

(1_minus g) . c >= 0 by Th1;
then A4: 1 - (g . c) >= 0 by FUZZY_1:def 6;
h . c <= f . c by A3, XXREAL_0:def 10;
then 1 - (h . c) >= 1 - (f . c) by XREAL_1:12;
then A5: (1 - (g . c)) * (1 - (f . c)) <= (1 - (g . c)) * (1 - (h . c)) by A4, XREAL_1:66;
(1_minus f) . c >= 0 by Th1;
then A6: 1 - (f . c) >= 0 by FUZZY_1:def 6;
f ++ f c= by Th33;
then (f ++ f) . c >= f . c by FUZZY_1:def 3;
then A7: ((f . c) + (f . c)) - ((f . c) * (f . c)) >= f . c by Def3;
g . c <= f . c by A3, XXREAL_0:def 10;
then 1 - (g . c) >= 1 - (f . c) by XREAL_1:12;
then (1 - (f . c)) * (1 - (f . c)) <= (1 - (g . c)) * (1 - (f . c)) by A6, XREAL_1:66;
then (1 - (f . c)) * (1 - (f . c)) <= (1 - (g . c)) * (1 - (h . c)) by A5, XXREAL_0:2;
then 1 - ((1 - (f . c)) * (1 - (f . c))) >= 1 - ((1 - (g . c)) * (1 - (h . c))) by XREAL_1:12;
hence max (f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))) <= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * (max (f . c),(h . c))) by A3, A7, XXREAL_0:28; :: thesis: verum

end;

suppose A8: ( max (f . c),(g . c) = f . c & max (f . c),(h . c) = h . c ) ; :: thesis: max (f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))) <= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * (max (f . c),(h . c)))

(1_minus f) . c >= 0 by Th1;
then A9: 1 - (f . c) >= 0 by FUZZY_1:def 6;
h . c >= 0 by Th1;
then 0 * (h . c) <= (h . c) * (1 - (f . c)) by A9, XREAL_1:66;
then A10: 0 + (f . c) <= ((h . c) * (1 - (f . c))) + (f . c) by XREAL_1:8;
(1_minus h) . c >= 0 by Th1;
then A11: 1 - (h . c) >= 0 by FUZZY_1:def 6;
g . c <= f . c by A8, XXREAL_0:def 10;
then 1 - (f . c) <= 1 - (g . c) by XREAL_1:12;
then (1 - (f . c)) * (1 - (h . c)) <= (1 - (g . c)) * (1 - (h . c)) by A11, XREAL_1:66;
then 1 - ((1 - (f . c)) * (1 - (h . c))) >= 1 - ((1 - (g . c)) * (1 - (h . c))) by XREAL_1:12;
hence max (f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))) <= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * (max (f . c),(h . c))) by A8, A10, XXREAL_0:28; :: thesis: verum

end;

suppose A12: ( max (f . c),(g . c) = g . c & max (f . c),(h . c) = f . c ) ; :: thesis: max (f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))) <= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * (max (f . c),(h . c)))

(1_minus f) . c >= 0 by Th1;
then A13: 1 - (f . c) >= 0 by FUZZY_1:def 6;
g . c >= 0 by Th1;
then 0 * (g . c) <= (g . c) * (1 - (f . c)) by A13, XREAL_1:66;
then A14: 0 + (f . c) <= ((g . c) * (1 - (f . c))) + (f . c) by XREAL_1:8;
(1_minus g) . c >= 0 by Th1;
then A15: 1 - (g . c) >= 0 by FUZZY_1:def 6;
h . c <= f . c by A12, XXREAL_0:def 10;
then 1 - (f . c) <= 1 - (h . c) by XREAL_1:12;
then (1 - (f . c)) * (1 - (g . c)) <= (1 - (h . c)) * (1 - (g . c)) by A15, XREAL_1:66;
then 1 - ((1 - (f . c)) * (1 - (g . c))) >= 1 - ((1 - (h . c)) * (1 - (g . c))) by XREAL_1:12;
hence max (f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))) <= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * (max (f . c),(h . c))) by A12, A14, XXREAL_0:28; :: thesis: verum

end;

suppose A16: ( max (f . c),(g . c) = g . c & max (f . c),(h . c) = h . c ) ; :: thesis: max (f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))) <= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * (max (f . c),(h . c)))

(1_minus g) . c >= 0 by Th1;
then A17: 1 - (g . c) >= 0 by FUZZY_1:def 6;
h . c >= f . c by A16, XXREAL_0:def 10;
then 1 - (h . c) <= 1 - (f . c) by XREAL_1:12;
then A18: (1 - (g . c)) * (1 - (f . c)) >= (1 - (g . c)) * (1 - (h . c)) by A17, XREAL_1:66;
(1_minus f) . c >= 0 by Th1;
then A19: 1 - (f . c) >= 0 by FUZZY_1:def 6;
g . c >= f . c by A16, XXREAL_0:def 10;
then 1 - (g . c) <= 1 - (f . c) by XREAL_1:12;
then (1 - (f . c)) * (1 - (f . c)) >= (1 - (g . c)) * (1 - (f . c)) by A19, XREAL_1:66;
then (1 - (f . c)) * (1 - (f . c)) >= (1 - (g . c)) * (1 - (h . c)) by A18, XXREAL_0:2;
then 1 - ((1 - (f . c)) * (1 - (f . c))) <= 1 - ((1 - (g . c)) * (1 - (h . c))) by XREAL_1:12;
then A20: (f ++ f) . c <= 1 - ((1 - (g . c)) * (1 - (h . c))) by Th54;
f ++ f c= by Th33;
then (f ++ f) . c >= f . c by FUZZY_1:def 3;
then f . c <= 1 - ((1 - (g . c)) * (1 - (h . c))) by A20, XXREAL_0:2;
hence max (f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))) <= ((max (f . c),(g . c)) + (max (f . c),(h . c))) - ((max (f . c),(g . c)) * (max (f . c),(h . c))) by A16, XXREAL_0:28; :: thesis: verum

end;

end;

end;

(max f,(g ++ h)) . c = max (f . c),((g ++ h) . c) by FUZZY_1:6
.= max (f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))) by Th54 ;
hence (max f,(g ++ h)) . c <= ((max f,g) ++ (max f,h)) . c by A1, A2; :: thesis: verum