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