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