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

let x be set ; :: 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 set such that
A1: [x,y] in S by RELAT_1:def 4;
( x in X & x = y ) by A1, RELAT_1:def 10;
hence x in proj2 S by A1, RELAT_1:def 5; :: thesis: verum

end;

assume x in proj2 S ; :: thesis: x in proj1 S
then consider y being set such that
A2: [y,x] in S by RELAT_1:def 5;
( y in X & x = y ) by A2, RELAT_1:def 10;
hence x in proj1 S by A2, RELAT_1:def 4; :: thesis: verum

end;

hence proj1 S = proj2 S by TARSKI:2; :: thesis: verum