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

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

.= min (f,(max ((1_minus (max (g,h))),(min (g,h))))) by FUZZY_1:9 ;

hence f \ (g \+\ h) c= by Th21, FUZZY_1:25; :: thesis: verum

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

.= min (f,(max ((1_minus (max (g,h))),(min (g,h))))) by FUZZY_1:9 ;

hence f \ (g \+\ h) c= by Th21, FUZZY_1:25; :: thesis: verum