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 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 5
.= (pr2 the carrier of T,the carrier of T) . x,y by A3, A6, 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, A5; :: 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
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 set 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 5
.= y by A9, A10, A12, FUNCT_3:def 6 ;
hence a in id the carrier of T by A7, A9, A11, RELAT_1:def 10; :: thesis: verum