:: deftheorem defines [ XTUPLE_0:def 4 :
for x1, x2, x3 being object holds [x1,x2,x3] = [[x1,x2],x3];