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