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
for X being Subset of st x in X & X is open holds
ex Y being Subset of 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 ; :: 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 ; :: 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 A3: ( x in X & 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 by A1;
consider B being Subset of such that
A4: ( x in Int B & B c= A & B is compact ) by A1, A2, A3, TOPS_3:76;
reconsider Y = B as Subset of 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, A4, Th26, TOPS_3:77; :: thesis: verum