:: deftheorem Def10 defines PairSetFamily PENCIL_4:def 10 :
for X being set
for L being Subset-Family of X
for b₃ being Subset-Family of (PairSet X) holds
( b₃ = PairSetFamily L iff for S being set holds
( S in b₃ iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) );