let A, X, B 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 set holds
( x in A iff x in B )

proof

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

end;

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