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:40

.= f by FUZZY_1:18 ; :: thesis: verum

let f be Membership_Func of C; :: thesis: f \ (EMF C) = f

thus f \ (EMF C) = min (f,(UMF C)) by FUZZY_1:40

.= f by FUZZY_1:18 ; :: thesis: verum