let X be set ; :: thesis: for V being Subset of X holds
( (chi (V,X)) " {1} = V & (chi (V,X)) " {0} = X \ V )
let V be Subset of X; :: thesis: ( (chi (V,X)) " {1} = V & (chi (V,X)) " {0} = X \ V )
thus (chi (V,X)) " {1} = V :: thesis: (chi (V,X)) " {0} = X \ V

proof

thus (chi (V,X)) " {1} c= V :: according to XBOOLE_0:def 10 :: thesis: V c= (chi (V,X)) " {1}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (chi (V,X)) " {1} or x in V )
reconsider xx = x as set by TARSKI:1;
assume A1: x in (chi (V,X)) " {1} ; :: thesis: x in V
then (chi (V,X)) . x in {1} by FUNCT_1:def 7;
then (chi (V,X)) . xx = {0} by TARSKI:def 1, CARD_1:49;
then (chi (V,X)) . xx <> {} ;
hence x in V by A1, FUNCT_3:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V or x in (chi (V,X)) " {1} )
assume A2: x in V ; :: thesis: x in (chi (V,X)) " {1}
then (chi (V,X)) . x = 1 by FUNCT_3:def 3;
then A3: (chi (V,X)) . x in {1} by TARSKI:def 1;
x in X by A2;
then x in dom (chi (V,X)) by FUNCT_3:def 3;
hence x in (chi (V,X)) " {1} by A3, FUNCT_1:def 7; :: thesis: verum

end;

thus (chi (V,X)) " {0} = X \ V :: thesis: verum

proof

thus (chi (V,X)) " {0} c= X \ V :: according to XBOOLE_0:def 10 :: thesis: X \ V c= (chi (V,X)) " {0}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (chi (V,X)) " {0} or x in X \ V )
A4: ( x in V implies (chi (V,X)) . x = 1 ) by FUNCT_3:def 3;
assume A5: x in (chi (V,X)) " {0} ; :: thesis: x in X \ V
then (chi (V,X)) . x in {0} by FUNCT_1:def 7;
hence x in X \ V by A4, A5, TARSKI:def 1, XBOOLE_0:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ V or x in (chi (V,X)) " {0} )
assume A6: x in X \ V ; :: thesis: x in (chi (V,X)) " {0}
then not x in V by XBOOLE_0:def 5;
then (chi (V,X)) . x = 0 by A6, FUNCT_3:def 3;
then A7: (chi (V,X)) . x in {0} by TARSKI:def 1;
x in X by A6;
then x in dom (chi (V,X)) by FUNCT_3:def 3;
hence x in (chi (V,X)) " {0} by A7, FUNCT_1:def 7; :: thesis: verum

end;