let T be non empty TopSpace; :: thesis: ( T is regular implies ( T is locally-compact iff for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) ) )
assume A1: T is regular ; :: thesis: ( T is locally-compact iff for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) )
assume A3: for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) ; :: 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 ( 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 )
then A4: x in Int X by TOPS_1:23;
consider Y being Subset of T such that
A5: x in Int Y and
A6: Y is compact by A3;
x in (Int X) /\ (Int Y) by A5, A4, XBOOLE_0:def 4;
then x in Int (X /\ Y) by TOPS_1:17;
then consider Q being Subset of T such that
A7: Q is closed and
A8: Q c= X /\ Y and
A9: x in Int Q by A1, Th27;
take Q ; :: thesis: ( x in Int Q & Q c= X & Q is compact )
thus x in Int Q by A9; :: thesis: ( Q c= X & Q is compact )
X /\ Y c= X by XBOOLE_1:17;
hence Q c= X by A8; :: thesis: Q is compact
X /\ Y c= Y by XBOOLE_1:17;
hence Q is compact by A6, A7, A8, COMPTS_1:9, XBOOLE_1:1; :: thesis: verum