let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C holds f \ (g \+\ h) c=
let f, g, h be Membership_Func of C; :: thesis: f \ (g \+\ h) c=
max (f \ (max g,h)),(min (min f,g),h) = max (min f,(1_minus (max g,h))),(min f,(min g,h)) by FUZZY_1:8
.= min f,(max (1_minus (max g,h)),(min g,h)) by FUZZY_1:10 ;
hence f \ (g \+\ h) c= by Th26, FUZZY_1:28; :: thesis: verum