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