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)
proof
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;
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 ;
A2: B is basis of x
proof
let V be a_neighborhood of x; :: according to YELLOW13:def 2 :: thesis: ex b1 being a_neighborhood of x st
( b1 in B & b1 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 is compact
proof
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;
hence ex B being basis of x st B is compact by A2; :: thesis: verum