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