let X be non empty TopSpace; :: thesis: X,X | ([#] X) are_homeomorphic
set f = id X;
A1: dom (id X) = [#] X ;
A2: [#] (X | ([#] X)) = [#] X by PRE_TOPC:def 5;
A3: rng (id X) = [#] (X | ([#] X)) by PRE_TOPC:def 5;
reconsider XX = X | ([#] X) as non empty TopSpace ;
reconsider f = id X as Function of X,XX by A2;
ZZ: 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 A4: ([#] X) \ P in the topology of X by PRE_TOPC:def 2, PRE_TOPC:def 3;
A5: for x being object holds
( x in (f ") " P iff x in P )

proof

let x be object ; :: 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 object 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;

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

end;

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