let X be non empty regular TopSpace; :: thesis: ( X is locally-compact implies X is liminally-compact )

assume A1: X is locally-compact ; :: thesis: X is liminally-compact

let x be Point of X; :: according to COMPACT1:def 3 :: thesis: ex B being basis of x st B is compact

set B = { Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } ;

{ Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } c= bool ([#] X)

A2: B is basis of x

assume A1: X is locally-compact ; :: thesis: X is liminally-compact

let x be Point of X; :: according to COMPACT1:def 3 :: thesis: ex B being basis of x st B is compact

set B = { Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } ;

{ Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } c= bool ([#] X)

proof

then reconsider B = { Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } as Subset-Family of X ;
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in { Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } or A in bool ([#] X) )

assume A in { Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } ; :: thesis: A in bool ([#] X)

then ex Q being a_neighborhood of x st

( A = Q & Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) ;

hence A in bool ([#] X) ; :: thesis: verum

end;assume A in { Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } ; :: thesis: A in bool ([#] X)

then ex Q being a_neighborhood of x st

( A = Q & Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) ;

hence A in bool ([#] X) ; :: thesis: verum

A2: B is basis of x

proof

B is compact
let V be a_neighborhood of x; :: according to YELLOW13:def 2 :: thesis: ex b_{1} being a_neighborhood of x st

( b_{1} in B & b_{1} c= V )

A3: x in Int V by CONNSP_2:def 1;

consider W being a_neighborhood of x such that

A4: W is compact by A1;

x in Int W by CONNSP_2:def 1;

then x in (Int V) /\ (Int W) by A3, XBOOLE_0:def 4;

then x in Int (V /\ W) by TOPS_1:17;

then consider Q being Subset of X such that

A5: Q is closed and

A6: Q c= V /\ W and

A7: x in Int Q by YELLOW_8:27;

reconsider Q = Q as a_neighborhood of x by A7, CONNSP_2:def 1;

take Q ; :: thesis: ( Q in B & Q c= V )

V /\ W c= W by XBOOLE_1:17;

then Q is compact by A4, A5, A6, COMPTS_1:9, XBOOLE_1:1;

hence Q in B by A6; :: thesis: Q c= V

V /\ W c= V by XBOOLE_1:17;

hence Q c= V by A6; :: thesis: verum

end;( b

A3: x in Int V by CONNSP_2:def 1;

consider W being a_neighborhood of x such that

A4: W is compact by A1;

x in Int W by CONNSP_2:def 1;

then x in (Int V) /\ (Int W) by A3, XBOOLE_0:def 4;

then x in Int (V /\ W) by TOPS_1:17;

then consider Q being Subset of X such that

A5: Q is closed and

A6: Q c= V /\ W and

A7: x in Int Q by YELLOW_8:27;

reconsider Q = Q as a_neighborhood of x by A7, CONNSP_2:def 1;

take Q ; :: thesis: ( Q in B & Q c= V )

V /\ W c= W by XBOOLE_1:17;

then Q is compact by A4, A5, A6, COMPTS_1:9, XBOOLE_1:1;

hence Q in B by A6; :: thesis: Q c= V

V /\ W c= V by XBOOLE_1:17;

hence Q c= V by A6; :: thesis: verum

proof

hence
ex B being basis of x st B is compact
by A2; :: thesis: verum
let U be Subset of X; :: according to COMPACT1:def 1 :: thesis: ( U in B implies U is compact )

assume U in B ; :: thesis: U is compact

then ex Q being a_neighborhood of x st

( U = Q & Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) ;

hence U is compact ; :: thesis: verum

end;assume U in B ; :: thesis: U is compact

then ex Q being a_neighborhood of x st

( U = Q & Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) ;

hence U is compact ; :: thesis: verum