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