let x, X, A be set ; :: thesis: ( x in X \ A implies (chi (A,X)) . x = {} )
assume A1: x in X \ A ; :: thesis: (chi (A,X)) . x = {}
then not x in A by XBOOLE_0:def 5;
hence (chi (A,X)) . x = {} by A1, Def3; :: thesis: verum