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 ) )

hereby :: thesis: ( ( for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) ) implies T is locally-compact )
assume A2: T is locally-compact ; :: thesis: for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact )

let x be Point of T; :: thesis: ex Y being Subset of T st
( x in Int Y & Y is compact )

ex Y being Subset of T st
( x in Int Y & Y c= [#] T & Y is compact ) by A2;
hence ex Y being Subset of T st
( x in Int Y & Y is compact ) ; :: thesis: verum
end;
assume A3: for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) ; :: thesis:
let x be Point of T; :: according to WAYBEL_3:def 9 :: thesis: for b1 being Element of bool the carrier of T holds
( not x in b1 or not b1 is open or ex b2 being Element of bool the carrier of T st
( x in Int b2 & b2 c= b1 & b2 is compact ) )

let X be Subset of T; :: thesis: ( not x in X or not X is open or ex b1 being Element of bool the carrier of T st
( x in Int b1 & b1 c= X & b1 is compact ) )

assume ( x in X & X is open ) ; :: thesis: ex b1 being Element of bool the carrier of T st
( x in Int b1 & b1 c= X & b1 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 ;
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 ;
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 ; :: thesis: verum