hereby :: thesis: ( ( for x being Point of X ex B being basis of x st B is compact ) implies X is liminally-compact )

assume A6:
for x being Point of X ex B being basis of x st B is compact
; :: thesis: 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)

A2: B is basis of x

end;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

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 ;
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;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

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 )

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

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

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 being a_neighborhood of x st Q c= V ) ;

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 being a_neighborhood of x st Q c= V ) ;

hence U is compact ; :: thesis: verum

let x be Point of X; :: according to WAYBEL_3:def 9 :: thesis: for b

( not x in b

( x in Int b

let P be Subset of X; :: thesis: ( not x in P or not P is open or ex b

( x in Int b

assume that

A7: x in P and

A8: P is open ; :: thesis: ex b

( x in Int b

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