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