let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C holds (f \ g) \ h = f \ (max (g,h))

let f, h, g 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:7

.= f \ (max (g,h)) by FUZZY_1:11 ; :: thesis: verum

let f, h, g 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:7

.= f \ (max (g,h)) by FUZZY_1:11 ; :: thesis: verum