let C be non empty set ; :: thesis: for f being Membership_Func of C holds UMF C c=
let f be Membership_Func of C; :: thesis: UMF C c=
let x be Element of C; :: according to FUZZY_1:def 3 :: thesis: f . x <= (UMF C) . x
A1: dom f = C by FUNCT_2:def 1;
A2: (UMF C) . x = 1 by FUNCT_3:def 3;
rng f c= [.0 ,1.] by RELAT_1:def 19;
hence f . x <= (UMF C) . x by A1, A2, Th14; :: thesis: verum