let x be object ; :: thesis: ( x is quadruple implies x is triple )
given x1, x2, x3, x4 being object such that A1: x = [x1,x2,x3,x4] ; :: according to XTUPLE_0:def 9 :: thesis: x is triple
x = [[x1,x2],x3,x4] by A1;
hence x is triple ; :: thesis: verum