let X be set ; :: thesis: for C being non empty set
for c being Element of C holds
( c in C \ X iff (chi (X,C)) . c = 0 )
let C be non empty set ; :: thesis: for c being Element of C holds
( c in C \ X iff (chi (X,C)) . c = 0 )
let c be Element of C; :: thesis: ( c in C \ X iff (chi (X,C)) . c = 0 )
thus ( c in C \ X implies (chi (X,C)) . c = 0 ) :: thesis: ( (chi (X,C)) . c = 0 implies c in C \ X )

proof

assume c in C \ X ; :: thesis: (chi (X,C)) . c = 0
then not c in X by XBOOLE_0:def 5;
hence (chi (X,C)) . c = 0 by Th77; :: thesis: verum

end;

assume (chi (X,C)) . c = 0 ; :: thesis: c in C \ X
then not c in X by Th77;
hence c in C \ X by XBOOLE_0:def 5; :: thesis: verum