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: 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 A1, Th14; :: thesis: verum