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