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 b₁ being a_neighborhood of x st
( b₁ in B & b₁ 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 A3, CONNSP_2:def 1;
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: X is liminally-compact
let x be Point of X; :: according to WAYBEL_3:def 9 :: thesis: for b₁ being Element of K19( the carrier of X) holds
( not x in b₁ or not b₁ is open or ex b₂ being Element of K19( the carrier of X) st
( x in Int b₂ & b₂ c= b₁ & b₂ is compact ) )
let P be Subset of X; :: thesis: ( not x in P or not P is open or ex b₁ being Element of K19( the carrier of X) st
( x in Int b₁ & b₁ c= P & b₁ is compact ) )
assume that
A7: x in P and
A8: P is open ; :: thesis: ex b₁ being Element of K19( the carrier of X) st
( x in Int b₁ & b₁ c= P & b₁ is compact )
consider B being basis of x such that
A9: B is compact by A6;
x in Int P by A7, A8, TOPS_1:23;
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 A11, A12; :: thesis: Q is compact
thus Q is compact by A9, A10; :: thesis: verum