let A, B, X be set ; :: thesis: ( A c= X & B c= X & chi (A,X) = chi (B,X) implies A = B )
assume that
A1: A c= X and
A2: B c= X and
A3: chi (A,X) = chi (B,X) ; :: thesis: A = B
for x being object holds
( x in A iff x in B )

proof

let x be object ; :: thesis: ( x in A iff x in B )
thus ( x in A implies x in B ) :: thesis: ( x in B implies x in A )

proof

assume x in A ; :: thesis: x in B
then (chi (A,X)) . x = 1 by A1, Def3;
hence x in B by A3, Th36; :: thesis: verum

end;

assume x in B ; :: thesis: x in A
then (chi (B,X)) . x = 1 by A2, Def3;
hence x in A by A3, Th36; :: thesis: verum

end;

hence A = B by TARSKI:2; :: thesis: verum