take [ the object , the object ] ; :: thesis: [ the object , the object ] is pair
take the object ; :: according to XTUPLE_0:def 1 :: thesis: ex x2 being object st [ the object , the object ] = [ the object ,x2]
take the object ; :: thesis: [ the object , the object ] = [ the object , the object ]
thus [ the object , the object ] = [ the object , the object ] ; :: thesis: verum