:: deftheorem defines `2_4 XTUPLE_0:def 11 :
for x being object holds x `2_4 = ((x `1) `1) `2 ;