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 5;

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 set ; :: 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 set such that
A3: ( x in the carrier of T & y in the carrier of T & a = [x,y] ) by ZFMISC_1:def 2;
A4: x = y by A2, A3, RELAT_1:def 10;
(pr1 the carrier of T,the carrier of T) . x,y = x by A3, FUNCT_3:def 5
.= (pr2 the carrier of T,the carrier of T) . x,y by A3, A4, FUNCT_3:def 6 ;
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, A3; :: thesis: verum

end;

let a be set ; :: 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
A5: ( a = p & (pr1 the carrier of T,the carrier of T) . p = (pr2 the carrier of T,the carrier of T) . p ) ;
consider x, y being set such that
A6: ( x in the carrier of T & y in the carrier of T & p = [x,y] ) by A1, ZFMISC_1:def 2;
A7: (pr1 the carrier of T,the carrier of T) . x,y = (pr2 the carrier of T,the carrier of T) . x,y by A5, A6;
x = (pr1 the carrier of T,the carrier of T) . x,y by A6, FUNCT_3:def 5
.= y by A6, A7, FUNCT_3:def 6 ;
hence a in id the carrier of T by A5, A6, RELAT_1:def 10; :: thesis: verum