let A, B be set ; :: thesis: ( ( for z being object st z in A holds

ex x, y being object st z = [x,y] ) & ( for z being object st z in B holds

ex x, y being object st z = [x,y] ) & ( for x, y being object holds

( [x,y] in A iff [x,y] in B ) ) implies A = B )

assume that

A1: for z being object st z in A holds

ex x, y being object st z = [x,y] and

A2: for z being object st z in B holds

ex x, y being object st z = [x,y] and

A3: for x, y being object holds

( [x,y] in A iff [x,y] in B ) ; :: thesis: A = B

ex x, y being object st z = [x,y] ) & ( for z being object st z in B holds

ex x, y being object st z = [x,y] ) & ( for x, y being object holds

( [x,y] in A iff [x,y] in B ) ) implies A = B )

assume that

A1: for z being object st z in A holds

ex x, y being object st z = [x,y] and

A2: for z being object st z in B holds

ex x, y being object st z = [x,y] and

A3: for x, y being object holds

( [x,y] in A iff [x,y] in B ) ; :: thesis: A = B

now :: thesis: for z being object holds

( z in A iff z in B )

hence
A = B
by TARSKI:2; :: thesis: verum( z in A iff z in B )

let z be object ; :: thesis: ( z in A iff z in B )

A4: ( z in B implies ex x, y being object st z = [x,y] ) by A2;

( z in A implies ex x, y being object st z = [x,y] ) by A1;

hence ( z in A iff z in B ) by A3, A4; :: thesis: verum

end;A4: ( z in B implies ex x, y being object st z = [x,y] ) by A2;

( z in A implies ex x, y being object st z = [x,y] ) by A1;

hence ( z in A iff z in B ) by A3, A4; :: thesis: verum