theorem :: RFUNCT_1:64

for X being set
for C being non empty set
for c being Element of C holds
( not c in X iff (chi (X,C)) . c = 0 ) by Th61;