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