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