let T be non empty TopSpace; :: thesis: id the carrier of T = { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p }
set f = pr1 ( the carrier of T, the carrier of T);
set g = pr2 ( the carrier of T, the carrier of T);
A1: the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } c= id the carrier of T

let a be object ; :: thesis: ( a in id the carrier of T implies a in { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } )
assume A2: a in id the carrier of T ; :: thesis: a in { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p }
then consider x, y being object such that
A3: x in the carrier of T and
A4: y in the carrier of T and
A5: a = [x,y] by ZFMISC_1:def 2;
A6: x = y by A2, A5, RELAT_1:def 10;
(pr1 ( the carrier of T, the carrier of T)) . (x,y) = x by A3, A4, FUNCT_3:def 4
.= (pr2 ( the carrier of T, the carrier of T)) . (x,y) by A3, A6, FUNCT_3:def 5 ;
hence a in { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } by A1, A2, A5; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } or a in id the carrier of T )
assume a in { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } ; :: thesis: a in id the carrier of T
then consider p being Point of [:T,T:] such that
A7: a = p and
A8: (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p ;
consider x, y being object such that
A9: x in the carrier of T and
A10: y in the carrier of T and
A11: p = [x,y] by A1, ZFMISC_1:def 2;
A12: (pr1 ( the carrier of T, the carrier of T)) . (x,y) = (pr2 ( the carrier of T, the carrier of T)) . (x,y) by A8, A11;
x = (pr1 ( the carrier of T, the carrier of T)) . (x,y) by A9, A10, FUNCT_3:def 4
.= y by A9, A10, A12, FUNCT_3:def 5 ;
hence a in id the carrier of T by A7, A9, A11, RELAT_1:def 10; :: thesis: verum