let x, A, X be set ; :: thesis: ( (chi A,X) . x = 1 implies x in A )
assume A1: (chi A,X) . x = 1 ; :: thesis: x in A

per cases ( x in X or not x in X ) ;

suppose x in X ; :: thesis: x in A

hence x in A by A1, Def3; :: thesis: verum

end;

suppose not x in X ; :: thesis: x in A

then not x in dom (chi A,X) by Def3;
hence x in A by A1, FUNCT_1:def 4; :: thesis: verum

end;

end;