let C be non empty set ; :: thesis: for f being Membership_Func of C holds f \ (EMF C) = f
let f be Membership_Func of C; :: thesis: f \ (EMF C) = f
thus f \ (EMF C) = min f,(UMF C) by FUZZY_1:44
.= f by FUZZY_1:19 ; :: thesis: verum