hereby :: thesis: ( ( for x being Point of X ex B being basis of x st B is compact ) implies X is liminally-compact )
assume A1: X is liminally-compact ; :: thesis: for x being Point of X ex B being basis of x st B is compact
let x be Point of X; :: 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 being a_neighborhood of x st Q c= V ) } ;
{ Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V ) } 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 being a_neighborhood of x st Q c= V ) } or A in bool ([#] X) )
assume A in { Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V ) } ; :: thesis: A in bool ([#] X)
then ex Q being a_neighborhood of x st
( A = Q & Q is compact & ex V being a_neighborhood of x st Q c= V ) ;
hence A in bool ([#] X) ; :: thesis: verum
end;
then reconsider B = { Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V ) } 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 )

x in Int V by CONNSP_2:def 1;
then consider Q being Subset of X such that
A3: x in Int Q and
A4: Q c= Int V and
A5: Q is compact by A1;
reconsider Q = Q as a_neighborhood of x by ;
take Q ; :: thesis: ( Q in B & Q c= V )
Int V c= V by TOPS_1:16;
hence ( Q in B & Q c= V ) by A4, A5; :: 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 being a_neighborhood of x st Q c= V ) ;
hence U is compact ; :: thesis: verum
end;
hence ex B being basis of x st B is compact by A2; :: thesis: verum
end;
assume A6: for x being Point of X ex B being basis of x st B is compact ; :: thesis:
let x be Point of X; :: according to WAYBEL_3:def 9 :: thesis: for b1 being Element of K19( the carrier of X) holds
( not x in b1 or not b1 is open or ex b2 being Element of K19( the carrier of X) st
( x in Int b2 & b2 c= b1 & b2 is compact ) )

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

assume that
A7: x in P and
A8: P is open ; :: thesis: ex b1 being Element of K19( the carrier of X) st
( x in Int b1 & b1 c= P & b1 is compact )

consider B being basis of x such that
A9: B is compact by A6;
x in Int P by ;
then consider Q being Subset of X such that
A10: Q in B and
A11: x in Int Q and
A12: Q c= P by YELLOW13:def 1;
take Q ; :: thesis: ( x in Int Q & Q c= P & Q is compact )
thus ( x in Int Q & Q c= P ) by ; :: thesis: Q is compact
thus Q is compact by ; :: thesis: verum