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

proof

now :: thesis: min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c))))

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

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

f ++ f c= by Th28;
then A4: (f ++ f) . c >= f . c ;
min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= f . c by XXREAL_0:17;
then min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= (f ++ f) . c by A4, XXREAL_0:2;
hence min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) by A3, Def3; :: thesis: verum

end;

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

(1_minus f) . c >= 0 by Th1;
then A6: 1 - (f . c) >= 0 by FUZZY_1:def 5;
h . c >= 0 by Th1;
then 0 * (h . c) <= (h . c) * (1 - (f . c)) by A6, XREAL_1:64;
then A7: 0 + (f . c) <= ((h . c) * (1 - (f . c))) + (f . c) by XREAL_1:6;
min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= f . c by XXREAL_0:17;
hence min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) by A5, A7, XXREAL_0:2; :: thesis: verum

end;

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

(1_minus f) . c >= 0 by Th1;
then A9: 1 - (f . c) >= 0 by FUZZY_1:def 5;
g . c >= 0 by Th1;
then 0 * (g . c) <= (g . c) * (1 - (f . c)) by A9, XREAL_1:64;
then A10: 0 + (f . c) <= ((g . c) * (1 - (f . c))) + (f . c) by XREAL_1:6;
min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= f . c by XXREAL_0:17;
hence min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) by A8, A10, XXREAL_0:2; :: thesis: verum

end;

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

hence min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) by XXREAL_0:17; :: thesis: verum

end;

end;

end;

hence min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) ; :: thesis: verum

end;

(min (f,(g ++ h))) . c = min ((f . c),((g ++ h) . c)) by FUZZY_1:5
.= min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) by Th49 ;
hence (min (f,(g ++ h))) . c <= ((min (f,g)) ++ (min (f,h))) . c by A1, A2; :: thesis: verum