let S, T be non empty TopSpace; :: thesis: ( TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & S is locally-compact implies T is locally-compact )
assume that
A1: TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) and
A2: for x being Point of S
for X being Subset of S st x in X & X is open holds
ex Y being Subset of S st
( x in Int Y & Y c= X & Y is compact ) ; :: according to WAYBEL_3:def 9 :: thesis: T is locally-compact
let x be Point of T; :: according to WAYBEL_3:def 9 :: thesis: for b₁ being Element of bool the carrier of T holds
( not x in b₁ or not b₁ is open or ex b₂ being Element of bool the carrier of T st
( x in Int b₂ & b₂ c= b₁ & b₂ is compact ) )
let X be Subset of T; :: thesis: ( not x in X or not X is open or ex b₁ being Element of bool the carrier of T st
( x in Int b₁ & b₁ c= X & b₁ is compact ) )
assume that
A3: x in X and
A4: X is open ; :: thesis: ex b₁ being Element of bool the carrier of T st
( x in Int b₁ & b₁ c= X & b₁ is compact )
reconsider A = X as Subset of S by A1;
A is open by A1, A4, TOPS_3:76;
then consider B being Subset of S such that
A5: ( x in Int B & B c= A & B is compact ) by A2, A3;
reconsider Y = B as Subset of T by A1;
take Y ; :: thesis: ( x in Int Y & Y c= X & Y is compact )
thus ( x in Int Y & Y c= X & Y is compact ) by A1, A5, Th26, TOPS_3:77; :: thesis: verum