( dom (chi A,X) = X & rng (chi A,X) c= [.0 ,1.] ) by FUNCT_3:def 3, FUZZY_1:1;
hence chi A,X is Membership_Func of X by FUZZY_1:def 1; :: thesis: verum