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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in (chi V,X) " {1} or x in V )
assume A1: x in (chi V,X) " {1} ; :: thesis: x in V
then (chi V,X) . x in {1} by FUNCT_1:def 13;
then (chi V,X) . x = 1 by TARSKI:def 1;
hence x in V by A1, FUNCT_3:def 3; :: thesis: verum

end;

let x be set ; :: 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 13; :: 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 set ; :: 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 13;
hence x in X \ V by A4, A5, TARSKI:def 1, XBOOLE_0:def 5; :: thesis: verum

end;

let x be set ; :: 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 13; :: thesis: verum

end;