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