:: deftheorem defines proj2_3 XTUPLE_0:def 15 :
for X being set holds proj2_3 X = proj2 (proj1 X);