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