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