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 } is Subset-Family of N

proof

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

proof

let k be set ; :: 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 consider A being Subset of N such that
A2: k = Cl A and
A in BO ;
thus k in bool the carrier of N by A2; :: thesis: verum

end;

hence { (Cl A) where A is Subset of N : A in BO } is Subset-Family of N ; :: thesis: verum

end;

then reconsider BC = { (Cl A) where A is Subset of N : A in BO } as Subset-Family of N ;
BC is basis of x

proof

let S be a_neighborhood of x; :: according to YELLOW13:def 2 :: thesis: ex b₁ being a_neighborhood of x st
( b₁ in BC & b₁ c= S )
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:22;
A5: ( x in W & W is open ) by A3, YELLOW_8:21;
then x in Int W by TOPS_1:55;
then reconsider T = W as a_neighborhood of x by CONNSP_2:def 1;
A6: Int S c= S by TOPS_1:44;

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

suppose A7: W <> [#] N ; :: thesis: ex b₁ being a_neighborhood of x st
( b₁ in BC & b₁ c= S )

x in W by A3, YELLOW_8:21;
then {x} c= W by ZFMISC_1:37;
then consider G being Subset of N such that
A8: G is open and
A9: {x} c= G and
A10: Cl G c= W by A5, A7, CONNSP_2:26;
x in G by A9, ZFMISC_1:37;
then consider K being Subset of N such that
A11: K in BO and
A12: K c= G by A8, YELLOW_8:22;
( x in K & K is open ) by A11, YELLOW_8:21;
then A13: x in Int K by TOPS_1:55;
Int K c= Int (Cl K) by PRE_TOPC:48, TOPS_1:48;
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 A11; :: thesis: KK c= S
Cl K c= Cl G by A12, PRE_TOPC:49;
then Cl K c= W by A10, XBOOLE_1:1;
then KK c= Int S by A4, XBOOLE_1:1;
hence KK c= S by A6, XBOOLE_1:1; :: thesis: verum

end;

suppose A14: W = [#] N ; :: thesis: ex b₁ being a_neighborhood of x st
( b₁ in BC & b₁ c= S )

take T ; :: thesis: ( T in BC & T c= S )
Cl ([#] N) = [#] N by TOPS_1:27;
hence T in BC by A3, A14; :: thesis: T c= S
thus T c= S by A4, A6, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

then reconsider BC = BC as 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:17; :: thesis: verum