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