let A, X be set ; :: thesis: rng (chi (A,X)) c= {{},1}
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (chi (A,X)) or y in {{},1} )
assume y in rng (chi (A,X)) ; :: thesis: y in {{},1}
then consider x being set such that
A1: x in dom (chi (A,X)) and
A2: y = (chi (A,X)) . x by FUNCT_1:def 5;
A3: ( x in A or not x in A ) ;
x in X by A1, Def3;
then ( y = {} or y = 1 ) by A2, A3, Def3;
hence y in {{},1} by TARSKI:def 2; :: thesis: verum