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

let f, g be Membership_Func of C; :: thesis: f \ (f \ g) c=

f \ (f \ g) = min (f,(max ((1_minus f),(1_minus (1_minus g))))) by FUZZY_1:11

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

hence f \ (f \ g) c= by FUZZY_1:17; :: thesis: verum

let f, g be Membership_Func of C; :: thesis: f \ (f \ g) c=

f \ (f \ g) = min (f,(max ((1_minus f),(1_minus (1_minus g))))) by FUZZY_1:11

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

hence f \ (f \ g) c= by FUZZY_1:17; :: thesis: verum