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