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:12
.= max (min f,(1_minus f)),(min f,g) by FUZZY_1:10 ;
hence f \ (f \ g) c= by FUZZY_1:18; :: thesis: verum