let C be non empty set ; 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; (min (f,g)) ++ (min (f,h)) c=
let c be Element of C; FUZZY_1:def 2 (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))))
(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; verum