let N be Hausdorff complete Lawson topological_semilattice with_open_semilattices TopLattice; :: thesis: N is with_compact_semilattices

let x be Point of N; :: according to WAYBEL30:def 3 :: thesis: ex J being basis of x st

for A being Subset of N st A in J holds

( subrelstr A is meet-inheriting & A is compact )

consider BO being Basis of x such that

A1: for A being Subset of N st A in BO holds

subrelstr A is meet-inheriting by Def4;

set BC = { (Cl A) where A is Subset of N : A in BO } ;

{ (Cl A) where A is Subset of N : A in BO } c= bool the carrier of N

BC is basis of x

take BC ; :: thesis: for A being Subset of N st A in BC holds

( subrelstr A is meet-inheriting & A is compact )

let A be Subset of N; :: thesis: ( A in BC implies ( subrelstr A is meet-inheriting & A is compact ) )

assume A in BC ; :: thesis: ( subrelstr A is meet-inheriting & A is compact )

then consider C being Subset of N such that

A15: A = Cl C and

A16: C in BO ;

subrelstr C is meet-inheriting by A1, A16;

hence subrelstr A is meet-inheriting by A15, Th31; :: thesis: A is compact

thus A is compact by A15, COMPTS_1:8; :: thesis: verum

let x be Point of N; :: according to WAYBEL30:def 3 :: thesis: ex J being basis of x st

for A being Subset of N st A in J holds

( subrelstr A is meet-inheriting & A is compact )

consider BO being Basis of x such that

A1: for A being Subset of N st A in BO holds

subrelstr A is meet-inheriting by Def4;

set BC = { (Cl A) where A is Subset of N : A in BO } ;

{ (Cl A) where A is Subset of N : A in BO } c= bool the carrier of N

proof

then reconsider BC = { (Cl A) where A is Subset of N : A in BO } as Subset-Family of N ;
let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in { (Cl A) where A is Subset of N : A in BO } or k in bool the carrier of N )

assume k in { (Cl A) where A is Subset of N : A in BO } ; :: thesis: k in bool the carrier of N

then ex A being Subset of N st

( k = Cl A & A in BO ) ;

hence k in bool the carrier of N ; :: thesis: verum

end;assume k in { (Cl A) where A is Subset of N : A in BO } ; :: thesis: k in bool the carrier of N

then ex A being Subset of N st

( k = Cl A & A in BO ) ;

hence k in bool the carrier of N ; :: thesis: verum

BC is basis of x

proof

then reconsider BC = BC as basis of x ;
let S be a_neighborhood of x; :: according to YELLOW13:def 2 :: thesis: ex b_{1} being a_neighborhood of x st

( b_{1} in BC & b_{1} c= S )

A2: Int S c= S by TOPS_1:16;

x in Int S by CONNSP_2:def 1;

then consider W being Subset of N such that

A3: W in BO and

A4: W c= Int S by YELLOW_8:13;

A5: W is open by A3, YELLOW_8:12;

x in W by A3, YELLOW_8:12;

then x in Int W by A5, TOPS_1:23;

then reconsider T = W as a_neighborhood of x by CONNSP_2:def 1;

end;( b

A2: Int S c= S by TOPS_1:16;

x in Int S by CONNSP_2:def 1;

then consider W being Subset of N such that

A3: W in BO and

A4: W c= Int S by YELLOW_8:13;

A5: W is open by A3, YELLOW_8:12;

x in W by A3, YELLOW_8:12;

then x in Int W by A5, TOPS_1:23;

then reconsider T = W as a_neighborhood of x by CONNSP_2:def 1;

per cases
( W <> [#] N or W = [#] N )
;

end;

suppose A6:
W <> [#] N
; :: thesis: ex b_{1} being a_neighborhood of x st

( b_{1} in BC & b_{1} c= S )

( b

x in W
by A3, YELLOW_8:12;

then {x} c= W by ZFMISC_1:31;

then consider G being Subset of N such that

A7: G is open and

A8: {x} c= G and

A9: Cl G c= W by A5, A6, CONNSP_2:20;

x in G by A8, ZFMISC_1:31;

then consider K being Subset of N such that

A10: K in BO and

A11: K c= G by A7, YELLOW_8:13;

A12: K is open by A10, YELLOW_8:12;

A13: Int K c= Int (Cl K) by PRE_TOPC:18, TOPS_1:19;

x in K by A10, YELLOW_8:12;

then x in Int K by A12, TOPS_1:23;

then reconsider KK = Cl K as a_neighborhood of x by A13, CONNSP_2:def 1;

take KK ; :: thesis: ( KK in BC & KK c= S )

thus KK in BC by A10; :: thesis: KK c= S

Cl K c= Cl G by A11, PRE_TOPC:19;

then Cl K c= W by A9;

then KK c= Int S by A4;

hence KK c= S by A2; :: thesis: verum

end;then {x} c= W by ZFMISC_1:31;

then consider G being Subset of N such that

A7: G is open and

A8: {x} c= G and

A9: Cl G c= W by A5, A6, CONNSP_2:20;

x in G by A8, ZFMISC_1:31;

then consider K being Subset of N such that

A10: K in BO and

A11: K c= G by A7, YELLOW_8:13;

A12: K is open by A10, YELLOW_8:12;

A13: Int K c= Int (Cl K) by PRE_TOPC:18, TOPS_1:19;

x in K by A10, YELLOW_8:12;

then x in Int K by A12, TOPS_1:23;

then reconsider KK = Cl K as a_neighborhood of x by A13, CONNSP_2:def 1;

take KK ; :: thesis: ( KK in BC & KK c= S )

thus KK in BC by A10; :: thesis: KK c= S

Cl K c= Cl G by A11, PRE_TOPC:19;

then Cl K c= W by A9;

then KK c= Int S by A4;

hence KK c= S by A2; :: thesis: verum

take BC ; :: thesis: for A being Subset of N st A in BC holds

( subrelstr A is meet-inheriting & A is compact )

let A be Subset of N; :: thesis: ( A in BC implies ( subrelstr A is meet-inheriting & A is compact ) )

assume A in BC ; :: thesis: ( subrelstr A is meet-inheriting & A is compact )

then consider C being Subset of N such that

A15: A = Cl C and

A16: C in BO ;

subrelstr C is meet-inheriting by A1, A16;

hence subrelstr A is meet-inheriting by A15, Th31; :: thesis: A is compact

thus A is compact by A15, COMPTS_1:8; :: thesis: verum