let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds f \ (min (f,g)) c=
let f, g be Membership_Func of C; :: thesis: f \ (min (f,g)) c=
f \ (min (f,g)) = min (f,(max ((1_minus f),(1_minus g)))) by FUZZY_1:11
.= max ((min (f,(1_minus f))),(f \ g)) by FUZZY_1:9 ;
hence f \ (min (f,g)) c= by FUZZY_1:17; :: thesis: verum