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