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

( 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_{1} being Element of bool the carrier of T holds

( not x in b_{1} or not b_{1} is open or ex b_{2} being Element of bool the carrier of T st

( x in Int b_{2} & b_{2} c= b_{1} & b_{2} is compact ) )

let X be Subset of T; :: thesis: ( not x in X or not X is open or ex b_{1} being Element of bool the carrier of T st

( x in Int b_{1} & b_{1} c= X & b_{1} is compact ) )

assume ( x in X & X is open ) ; :: thesis: ex b_{1} being Element of bool the carrier of T st

( x in Int b_{1} & b_{1} c= X & b_{1} 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

( 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 A3:
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;( 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

( 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

( not x in b

( x in Int b

let X be Subset of T; :: thesis: ( not x in X or not X is open or ex b

( x in Int b

assume ( x in X & X is open ) ; :: thesis: ex b

( x in Int b

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