let p1, p2 be set ; :: thesis: ( ( for z being set holds
( z in p1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) & ( for z being set holds
( z in p2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) implies p1 = p2 )
assume that
A3: for z being set holds
( z in p1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) and
A4: for z being set holds
( z in p2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ; :: thesis: p1 = p2

now :: thesis: for z being object holds
( z in p1 iff z in p2 )

let z be object ; :: thesis: ( z in p1 iff z in p2 )
( z in p1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) by A3;
hence ( z in p1 iff z in p2 ) by A4; :: thesis: verum

end;

hence p1 = p2 by TARSKI:2; :: thesis: verum