:: deftheorem defines proj1_3 XTUPLE_0:def 14 :
for X being set holds proj1_3 X = proj1 (proj1 X);