set X = the object ;
take [ the object , the object , the object , the object , the object ] ; :: thesis: [ the object , the object , the object , the object , the object ] is quintuple
take the object ; :: according to CLASSES5:def 2 :: thesis: ex x2, x3, x4, x5 being object st [ the object , the object , the object , the object , the object ] = [ the object ,x2,x3,x4,x5]
take the object ; :: thesis: ex x3, x4, x5 being object st [ the object , the object , the object , the object , the object ] = [ the object , the object ,x3,x4,x5]
take the object ; :: thesis: ex x4, x5 being object st [ the object , the object , the object , the object , the object ] = [ the object , the object , the object ,x4,x5]
take the object ; :: thesis: ex x5 being object st [ the object , the object , the object , the object , the object ] = [ the object , the object , the object , the object ,x5]
take the object ; :: thesis: [ the object , the object , 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 , the object , the object ] ; :: thesis: verum