let C be non empty set ; :: thesis: for f being Membership_Func of C st EMF C c= holds
f = EMF C
let f be Membership_Func of C; :: thesis: ( EMF C c= implies f = EMF C )
f c= by Th13;
hence ( EMF C c= implies f = EMF C ) by Lm1; :: thesis: verum