let C be non empty set ; 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; (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))))
; verum