let X be set ; :: thesis: for S being Subset of (id X) holds proj1 S = proj2 S
let S be Subset of (id X); :: thesis: proj1 S = proj2 S
now :: thesis: for x being object holds
( ( x in proj1 S implies x in proj2 S ) & ( x in proj2 S implies x in proj1 S ) )
let x be object ; :: thesis: ( ( x in proj1 S implies x in proj2 S ) & ( x in proj2 S implies x in proj1 S ) )
hereby :: thesis: ( x in proj2 S implies x in proj1 S )
assume x in proj1 S ; :: thesis: x in proj2 S
then consider y being object such that
A1: [x,y] in S by XTUPLE_0:def 12;
x = y by A1, RELAT_1:def 10;
hence x in proj2 S by A1, XTUPLE_0:def 13; :: thesis: verum
end;
assume x in proj2 S ; :: thesis: x in proj1 S
then consider y being object such that
A2: [y,x] in S by XTUPLE_0:def 13;
x = y by A2, RELAT_1:def 10;
hence x in proj1 S by A2, XTUPLE_0:def 12; :: thesis: verum
end;
hence proj1 S = proj2 S by TARSKI:2; :: thesis: verum