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 K6( the carrier of T) holds
( not x in b₁ or not b₁ is open or ex b₂ being Element of K6( 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 K6( 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 K6( the carrier of T) st
( x in Int b₁ & b₁ c= X & b₁ is compact )
reconsider A = X as Subset of S by A1;
consider B being Subset of S 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 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, A4, Th25, TOPS_3:77; :: thesis: verum