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