assume A1: X is liminally-compact ; :: thesis:
let x be Point of X; :: thesis:
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)

let A be object ; :: according to TARSKI:def 3 :: thesis:
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:
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:

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

let V be a_neighborhood of x; :: according to YELLOW13:def 2 :: thesis:
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:
Int V c= V by TOPS_1:16;
hence ( Q in B & Q c= V ) by A4, A5; :: thesis:

end;

let U be Subset of X; :: according to COMPACT1:def 1 :: thesis:
assume U in B ; :: thesis:
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:

end;

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:
let P be Subset of X; :: thesis:
assume that
A7: x in P and
A8: P is open ; :: thesis:
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:
thus ( x in Int Q & Q c= P ) by A11, A12; :: thesis:
thus Q is compact by A9, A10; :: thesis: