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