:: deftheorem defines proj2_4 XTUPLE_0:def 17 :
for X being set holds proj2_4 X = proj2 (proj1_3 X);