let X be non empty Hausdorff TopSpace; :: thesis: for E being non empty Subset of X st X | E is dense & X | E is locally-compact holds

X | E is open

let E be non empty Subset of X; :: thesis: ( X | E is dense & X | E is locally-compact implies X | E is open )

assume A1: ( X | E is dense & X | E is locally-compact ) ; :: thesis: X | E is open

A2: [#] (X | E) = E by PRE_TOPC:8;

Int E = E

X | E is open

let E be non empty Subset of X; :: thesis: ( X | E is dense & X | E is locally-compact implies X | E is open )

assume A1: ( X | E is dense & X | E is locally-compact ) ; :: thesis: X | E is open

A2: [#] (X | E) = E by PRE_TOPC:8;

Int E = E

proof

hence
X | E is open
by A2, TSEP_1:16; :: thesis: verum
thus
Int E c= E
by TOPS_1:16; :: according to XBOOLE_0:def 10 :: thesis: E c= Int E

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in E or a in Int E )

assume A3: a in E ; :: thesis: a in Int E

then reconsider x = a as Point of X ;

reconsider xx = x as Point of (X | E) by A3, PRE_TOPC:8;

set UE = { G where G is Subset of X : ( G is open & G c= E ) } ;

consider K being a_neighborhood of xx such that

A4: K is compact by A1;

reconsider KK = K as Subset of X by A2, XBOOLE_1:1;

A5: K c= [#] (X | E) ;

Int K in the topology of (X | E) by PRE_TOPC:def 2;

then consider G being Subset of X such that

A6: G in the topology of X and

A7: Int K = G /\ E by A2, PRE_TOPC:def 4;

A8: G is open by A6;

for P being Subset of (X | E) st P = KK holds

P is compact by A4;

then KK is compact by A5, COMPTS_1:2;

then A9: Cl (G /\ E) c= KK by A7, TOPS_1:5, TOPS_1:16;

E is dense by A1, A2, TEX_3:def 1;

then A10: Cl (G /\ E) = Cl G by A8, TOPS_1:46;

G c= Cl G by PRE_TOPC:18;

then G c= K by A10, A9;

then G c= E by A2, XBOOLE_1:1;

then A11: G in { G where G is Subset of X : ( G is open & G c= E ) } by A8;

A12: xx in Int K by CONNSP_2:def 1;

Int K c= G by A7, XBOOLE_1:17;

then a in union { G where G is Subset of X : ( G is open & G c= E ) } by A12, A11, TARSKI:def 4;

hence a in Int E by TEX_4:3; :: thesis: verum

end;let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in E or a in Int E )

assume A3: a in E ; :: thesis: a in Int E

then reconsider x = a as Point of X ;

reconsider xx = x as Point of (X | E) by A3, PRE_TOPC:8;

set UE = { G where G is Subset of X : ( G is open & G c= E ) } ;

consider K being a_neighborhood of xx such that

A4: K is compact by A1;

reconsider KK = K as Subset of X by A2, XBOOLE_1:1;

A5: K c= [#] (X | E) ;

Int K in the topology of (X | E) by PRE_TOPC:def 2;

then consider G being Subset of X such that

A6: G in the topology of X and

A7: Int K = G /\ E by A2, PRE_TOPC:def 4;

A8: G is open by A6;

for P being Subset of (X | E) st P = KK holds

P is compact by A4;

then KK is compact by A5, COMPTS_1:2;

then A9: Cl (G /\ E) c= KK by A7, TOPS_1:5, TOPS_1:16;

E is dense by A1, A2, TEX_3:def 1;

then A10: Cl (G /\ E) = Cl G by A8, TOPS_1:46;

G c= Cl G by PRE_TOPC:18;

then G c= K by A10, A9;

then G c= E by A2, XBOOLE_1:1;

then A11: G in { G where G is Subset of X : ( G is open & G c= E ) } by A8;

A12: xx in Int K by CONNSP_2:def 1;

Int K c= G by A7, XBOOLE_1:17;

then a in union { G where G is Subset of X : ( G is open & G c= E ) } by A12, A11, TARSKI:def 4;

hence a in Int E by TEX_4:3; :: thesis: verum