take [ the object , the object , the object , the object ] ; :: thesis: [ the object , the object , the object , the object ] is quadruple
take the object ; :: according to XTUPLE_0:def 9 :: thesis: ex x2, x3, x4 being object st [ the object , the object , the object , the object ] = [ the object ,x2,x3,x4]
take the object ; :: thesis: ex x3, x4 being object st [ the object , the object , the object , the object ] = [ the object , the object ,x3,x4]
take the object ; :: thesis: ex x4 being object st [ the object , the object , the object , the object ] = [ the object , the object , the object ,x4]
take the object ; :: thesis: [ the object , the object , the object , the object ] = [ the object , the object , the object , the object ]
thus [ the object , the object , the object , the object ] = [ the object , the object , the object , the object ] ; :: thesis: verum