:: deftheorem Def13 defines proj2 XTUPLE_0:def 13 :
for X, b₂ being set holds
( b₂ = proj2 X iff for x being object holds
( x in b₂ iff ex y being object st [y,x] in X ) );