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 ;
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 ;
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 ; :: 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 ;
hence x in (f ") " P by ; :: thesis: verum
end;
S1: ([#] X) \ P = ([#] (X | ([#] X))) \ ((f ") " P) by ;
([#] X) \ P = (([#] X) /\ ([#] X)) \ P
.= (([#] X) \ P) /\ ([#] X) by XBOOLE_1:49 ;
then ([#] X) \ P in the topology of (X | ([#] X)) by ;
then ([#] (X | ([#] X))) \ ((f ") " P) is open by ;
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 ;
then f is being_homeomorphism by ;
hence X,X | ([#] X) are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum