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