let S, T be non empty TopSpace; ( 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 )
; WAYBEL_3:def 9 T is locally-compact
let x be Point of T; WAYBEL_3:def 9 for b1 being Element of K6( the carrier of T) holds
( not x in b1 or not b1 is open or ex b2 being Element of K6( the carrier of T) st
( x in Int b2 & b2 c= b1 & b2 is compact ) )
let X be Subset of T; ( not x in X or not X is open or ex b1 being Element of K6( the carrier of T) st
( x in Int b1 & b1 c= X & b1 is compact ) )
assume A3:
( x in X & X is open )
; ex b1 being Element of K6( the carrier of T) st
( x in Int b1 & b1 c= X & b1 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
; ( 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; verum