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