let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C holds (f \+\ g) \ h = max ((f \ (max (g,h))),(g \ (max (f,h))))
let f, h, g be Membership_Func of C; :: thesis: (f \+\ g) \ h = max ((f \ (max (g,h))),(g \ (max (f,h))))
set f1 = 1_minus f;
set g1 = 1_minus g;
set h1 = 1_minus h;
(max ((min (f,(1_minus g))),(min ((1_minus f),g)))) \ h = max ((min ((1_minus h),(min (f,(1_minus g))))),(min ((1_minus h),(min ((1_minus f),g))))) by FUZZY_1:9
.= max ((min ((min ((1_minus h),(1_minus g))),f)),(min ((1_minus h),(min ((1_minus f),g))))) by FUZZY_1:7
.= max ((min ((min ((1_minus h),(1_minus g))),f)),(min ((min ((1_minus h),(1_minus f))),g))) by FUZZY_1:7
.= max ((min (f,(1_minus (max (h,g))))),(min (g,(min ((1_minus h),(1_minus f)))))) by FUZZY_1:11
.= max ((f \ (max (h,g))),(g \ (max (f,h)))) by FUZZY_1:11 ;
hence (f \+\ g) \ h = max ((f \ (max (g,h))),(g \ (max (f,h)))) ; :: thesis: verum