:: deftheorem Def8 defines PairSet PENCIL_4:def 8 :
for X, b₂ being set holds
( b₂ = PairSet X iff for z being set holds
( z in b₂ iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) );