let A, X1, Y1, B, X2, Y2 be set ; :: thesis: ( A c= [:X1,Y1:] & B c= [:X2,Y2:] & ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) implies A = B )
assume that
A1: A c= [:X1,Y1:] and
A2: B c= [:X2,Y2:] and
A3: for x, y being set holds
( [x,y] in A iff [x,y] in B ) ; :: thesis: A = B

now :: thesis: for z being set holds
( z in A iff z in B )

let z be set ; :: thesis: ( z in A iff z in B )
A4: ( z in B implies ex x, y being set st
( x in X2 & y in Y2 & z = [x,y] ) ) by A2, Th84;
( z in A implies ex x, y being set st
( x in X1 & y in Y1 & z = [x,y] ) ) by A1, Th84;
hence ( z in A iff z in B ) by A3, A4; :: thesis: verum

end;

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