let p1, p2 be Subset-Family of (PairSet X); :: thesis: ( ( for S being set holds
( S in p1 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) ) & ( for S being set holds
( S in p2 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) ) implies p1 = p2 )
assume that
A5: for z being set holds
( z in p1 iff ex t being set ex l being Subset of X st
( t in X & l in L & z = PairSet (t,l) ) ) and
A6: for z being set holds
( z in p2 iff ex t being set ex l being Subset of X st
( t in X & l in L & z = PairSet (t,l) ) ) ; :: 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 t being set ex l being Subset of X st
( t in X & l in L & z = PairSet (t,l) ) ) by A5;
hence ( z in p1 iff z in p2 ) by A6; :: thesis: verum

end;

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