let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C holds (f \+\ g) \ h = max (f \ (max g,h)),(g \ (max f,h))
let f, g, h 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:10
.= max (min (min (1_minus h),(1_minus g)),f),(min (1_minus h),(min (1_minus f),g)) by FUZZY_1:8
.= max (min (min (1_minus h),(1_minus g)),f),(min (min (1_minus h),(1_minus f)),g) by FUZZY_1:8
.= max (min f,(1_minus (max h,g))),(min g,(min (1_minus h),(1_minus f))) by FUZZY_1:12
.= max (f \ (max h,g)),(g \ (max f,h)) by FUZZY_1:12 ;
hence (f \+\ g) \ h = max (f \ (max g,h)),(g \ (max f,h)) ; :: thesis: verum