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