:: deftheorem Def9 defines PairSet PENCIL_4:def 9 :
for t being object
for X, b₃ being set holds
( b₃ = PairSet (t,X) iff for z being set holds
( z in b₃ iff ex y being set st
( y in X & z = {t,y} ) ) );