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