let p1, p2 be set ; :: thesis: ( ( for z being set holds
( z in p1 iff ex y being set st
( y in X & z = {t,y} ) ) ) & ( for z being set holds
( z in p2 iff ex y being set st
( y in X & z = {t,y} ) ) ) implies p1 = p2 )
assume that
A6: for z being set holds
( z in p1 iff ex y being set st
( y in X & z = {t,y} ) ) and
A7: for z being set holds
( z in p2 iff ex y being set st
( y in X & z = {t,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 y being set st
( y in X & z = {t,y} ) ) by A6;
hence ( z in p1 iff z in p2 ) by A7; :: thesis: verum

end;

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