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
proof
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;
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 b1 being a_neighborhood of x st
( b1 in BC & b1 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;
per cases ( W <> [#] N or W = [#] N ) ;
suppose A6: W <> [#] N ; :: thesis: ex b1 being a_neighborhood of x st
( b1 in BC & b1 c= S )
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;
suppose A14: W = [#] N ; :: thesis: ex b1 being a_neighborhood of x st
( b1 in BC & b1 c= S )
take T ; :: thesis: ( T in BC & T c= S )
Cl ([#] N) = [#] N by TOPS_1:2;
hence T in BC by A3, A14; :: thesis: T c= S
thus T c= S by A4, A2; :: 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:8; :: thesis: verum