let X be non empty TopSpace; :: thesis: X,X | ([#] X) are_homeomorphic
set f = id X;
A1: dom (id X) = [#] X by RELAT_1:45;
A2: [#] (X | ([#] X)) = the carrier of TopStruct(# the carrier of X, the topology of X #) by TSEP_1:93
.= [#] X ;
then A3: rng (id X) = [#] (X | ([#] X)) by RELAT_1:45;
reconsider f = id X as Function of X,(X | ([#] X)) by A2;
for P being Subset of X st P is closed holds
(f ") " P is closed

proof

let P be Subset of X; :: thesis: ( P is closed implies (f ") " P is closed )
assume P is closed ; :: thesis: (f ") " P is closed
then ([#] X) \ P is open by PRE_TOPC:def 3;
then A4: ([#] X) \ P in the topology of X by PRE_TOPC:def 2;
A5: for x being set holds
( x in (f ") " P iff x in P )

proof

let x be set ; :: thesis: ( x in (f ") " P iff x in P )

hereby :: thesis: ( x in P implies x in (f ") " P )

assume A6: x in (f ") " P ; :: thesis: x in P
x in f .: P by A6, A3, TOPS_2:54;
then consider y being set such that
A7: ( [y,x] in f & y in P ) by RELAT_1:def 13;
thus x in P by A7, RELAT_1:def 10; :: thesis: verum

end;

assume A8: x in P ; :: thesis: x in (f ") " P
then [x,x] in id X by RELAT_1:def 10;
then x in f .: P by A8, RELAT_1:def 13;
hence x in (f ") " P by A3, TOPS_2:54; :: thesis: verum

end;

A9: ([#] X) \ P = ([#] (X | ([#] X))) \ ((f ") " P) by A2, A5, TARSKI:1;
([#] X) \ P = (([#] X) /\ ([#] X)) \ P
.= (([#] X) \ P) /\ ([#] X) by XBOOLE_1:49 ;
then ([#] X) \ P in the topology of (X | ([#] X)) by A2, A4, PRE_TOPC:def 4;
then ([#] (X | ([#] X))) \ ((f ") " P) is open by A9, PRE_TOPC:def 2;
hence (f ") " P is closed by PRE_TOPC:def 3; :: thesis: verum

end;

then A10: f " is continuous by PRE_TOPC:def 6;
f is continuous by JGRAPH_1:45;
then f is being_homeomorphism by A1, A3, A10, TOPS_2:def 5;
hence X,X | ([#] X) are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum