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 2 :: thesis: f . x <= (UMF C) . x
A1: 0 in REAL by XREAL_0:def 1;
A2: rng f c= [.0,1.] by RELAT_1:def 19;
( dom f = C & (UMF C) . x = 1 ) by FUNCT_2:def 1, FUNCT_3:def 3;
hence f . x <= (UMF C) . x by A2, Th12, A1; :: thesis: verum