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

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

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

S0:
f is continuous
by JGRAPH_1:45;
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 )

([#] 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;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

S1:
([#] X) \ P = ([#] (X | ([#] X))) \ ((f ") " P)
by A2, A5, TARSKI:2;
let x be object ; :: thesis: ( x in (f ") " P iff x in 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;hereby :: thesis: ( x in P implies x in (f ") " P )

assume A8:
x in P
; :: thesis: x in (f ") " Passume 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;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

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

([#] 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

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