:: Bases of Continuous Lattices
:: by Robert Milewski
::
:: Received November 28, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

theorem Th1: :: WAYBEL23:1
for L being non empty Poset
for x being Element of L holds compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L)
proofend;

definition
let L be non empty reflexive transitive RelStr ;
let X be Subset of (InclPoset (Ids L));
:: original:union
redefine func union X ->  Subset of L;
coherence
 union X is Subset of L
proofend;
end;

Lm1:  for X being non empty set
for Y being Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds
union Y c= sup Y
proofend;

theorem Th2: :: WAYBEL23:2
for L being non empty RelStr
for X, Y being Subset of L st X c= Y holds
finsups X c= finsups Y
proofend;

theorem Th3: :: WAYBEL23:3
for L being non empty transitive RelStr
for S being non empty full sups-inheriting SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X c= finsups Y
proofend;

theorem :: WAYBEL23:4
for L being non empty transitive antisymmetric complete RelStr
for S being non empty full sups-inheriting SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups X = finsups Y
proofend;

theorem Th5: :: WAYBEL23:5
for L being complete sup-Semilattice
for S being non empty full join-inheriting SubRelStr of L st Bottom L in the carrier of S holds
for X being Subset of L
for Y being Subset of S st X = Y holds
finsups Y c= finsups X
proofend;

theorem Th6: :: WAYBEL23:6
for L being lower-bounded sup-Semilattice
for X being Subset of (InclPoset (Ids L)) holds sup X = downarrow (finsups (union X))
proofend;

theorem Th7: :: WAYBEL23:7
for L being reflexive transitive RelStr
for X being Subset of L holds downarrow (downarrow X) = downarrow X
proofend;

theorem :: WAYBEL23:8
for L being reflexive transitive RelStr
for X being Subset of L holds uparrow (uparrow X) = uparrow X
proofend;

theorem :: WAYBEL23:9
for L being non empty reflexive transitive RelStr
for x being Element of L holds downarrow (downarrow x) = downarrow x
proofend;

theorem :: WAYBEL23:10
for L being non empty reflexive transitive RelStr
for x being Element of L holds uparrow (uparrow x) = uparrow x
proofend;

theorem Th11: :: WAYBEL23:11
for L being non empty RelStr
for S being non empty SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
downarrow Y c= downarrow X
proofend;

theorem Th12: :: WAYBEL23:12
for L being non empty RelStr
for S being non empty SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
uparrow Y c= uparrow X
proofend;

theorem :: WAYBEL23:13
for L being non empty RelStr
for S being non empty SubRelStr of L
for x being Element of L
for y being Element of S st x = y holds
downarrow y c= downarrow x
proofend;

theorem :: WAYBEL23:14
for L being non empty RelStr
for S being non empty SubRelStr of L
for x being Element of L
for y being Element of S st x = y holds
uparrow y c= uparrow x
proofend;

begin

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is meet-closed  means :Def1: :: WAYBEL23:def 1
 subrelstr S is meet-inheriting ;
end;

:: deftheorem Def1 defines meet-closed WAYBEL23:def_1_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is meet-closed iff subrelstr S is meet-inheriting );

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is join-closed  means :Def2: :: WAYBEL23:def 2
 subrelstr S is join-inheriting ;
end;

:: deftheorem Def2 defines join-closed WAYBEL23:def_2_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is join-closed iff subrelstr S is join-inheriting );

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is infs-closed  means :Def3: :: WAYBEL23:def 3
 subrelstr S is infs-inheriting ;
end;

:: deftheorem Def3 defines infs-closed WAYBEL23:def_3_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is infs-closed iff subrelstr S is infs-inheriting );

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is sups-closed  means :Def4: :: WAYBEL23:def 4
 subrelstr S is sups-inheriting ;
end;

:: deftheorem Def4 defines sups-closed WAYBEL23:def_4_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is sups-closed iff subrelstr S is sups-inheriting );

registration
let L be non empty RelStr ;
cluster infs-closed  ->  meet-closed for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is infs-closed holds
b1 is meet-closed
proofend;
cluster sups-closed  ->  join-closed for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is sups-closed holds
b1 is join-closed
proofend;
end;

registration
let L be non empty RelStr ;
cluster non empty infs-closed sups-closed for Element of K32( the carrier of L);
existence
 ex b1 being Subset of L st
( b1 is infs-closed & b1 is sups-closed & not b1 is empty )
proofend;
end;

theorem Th15: :: WAYBEL23:15
for L being non empty RelStr
for S being Subset of L holds
( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
inf {x,y} in S )
proofend;

theorem Th16: :: WAYBEL23:16
for L being non empty RelStr
for S being Subset of L holds
( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S )
proofend;

theorem :: WAYBEL23:17
for L being antisymmetric with_infima RelStr
for S being Subset of L holds
( S is meet-closed iff for x, y being Element of L st x in S & y in S holds
inf {x,y} in S )
proofend;

theorem Th18: :: WAYBEL23:18
for L being antisymmetric with_suprema RelStr
for S being Subset of L holds
( S is join-closed iff for x, y being Element of L st x in S & y in S holds
sup {x,y} in S )
proofend;

theorem :: WAYBEL23:19
for L being non empty RelStr
for S being Subset of L holds
( S is infs-closed iff for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S )
proofend;

theorem :: WAYBEL23:20
for L being non empty RelStr
for S being Subset of L holds
( S is sups-closed iff for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in S )
proofend;

theorem Th21: :: WAYBEL23:21
for L being non empty transitive RelStr
for S being non empty infs-closed Subset of L
for X being Subset of S st ex_inf_of X,L holds
( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) )
proofend;

theorem Th22: :: WAYBEL23:22
for L being non empty transitive RelStr
for S being non empty sups-closed Subset of L
for X being Subset of S st ex_sup_of X,L holds
( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )
proofend;

theorem :: WAYBEL23:23
for L being non empty transitive RelStr
for S being non empty meet-closed Subset of L
for x, y being Element of S st ex_inf_of {x,y},L holds
( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )
proofend;

theorem :: WAYBEL23:24
for L being non empty transitive RelStr
for S being non empty join-closed Subset of L
for x, y being Element of S st ex_sup_of {x,y},L holds
( ex_sup_of {x,y}, subrelstr S & "\/" ({x,y},(subrelstr S)) = "\/" ({x,y},L) )
proofend;

theorem Th25: :: WAYBEL23:25
for L being transitive antisymmetric with_infima RelStr
for S being non empty meet-closed Subset of L holds subrelstr S is with_infima
proofend;

theorem Th26: :: WAYBEL23:26
for L being transitive antisymmetric with_suprema RelStr
for S being non empty join-closed Subset of L holds subrelstr S is with_suprema
proofend;

registration
let L be transitive antisymmetric with_infima RelStr ;
let S be non empty meet-closed Subset of L;
cluster subrelstr S ->  with_infima ;
coherence
 subrelstr S is with_infima by Th25;
end;

registration
let L be transitive antisymmetric with_suprema RelStr ;
let S be non empty join-closed Subset of L;
cluster subrelstr S ->  with_suprema ;
coherence
 subrelstr S is with_suprema by Th26;
end;

theorem :: WAYBEL23:27
for L being non empty transitive antisymmetric complete RelStr
for S being non empty infs-closed Subset of L
for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)
proofend;

theorem :: WAYBEL23:28
for L being non empty transitive antisymmetric complete RelStr
for S being non empty sups-closed Subset of L
for X being Subset of S holds "\/" (X,(subrelstr S)) = "\/" (X,L)
proofend;

theorem Th29: :: WAYBEL23:29
for L being Semilattice
for S being meet-closed Subset of L holds S is filtered
proofend;

theorem Th30: :: WAYBEL23:30
for L being sup-Semilattice
for S being join-closed Subset of L holds S is directed
proofend;

registration
let L be Semilattice;
cluster meet-closed  ->  filtered for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is meet-closed holds
b1 is filtered by Th29;
end;

registration
let L be sup-Semilattice;
cluster join-closed  ->  directed for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is join-closed holds
b1 is directed by Th30;
end;

theorem :: WAYBEL23:31
for L being Semilattice
for S being non empty upper Subset of L holds
( S is Filter of L iff S is meet-closed )
proofend;

theorem :: WAYBEL23:32
for L being sup-Semilattice
for S being non empty lower Subset of L holds
( S is Ideal of L iff S is join-closed )
proofend;

theorem Th33: :: WAYBEL23:33
for L being non empty RelStr
for S1, S2 being join-closed Subset of L holds S1 /\ S2 is join-closed
proofend;

theorem :: WAYBEL23:34
for L being non empty RelStr
for S1, S2 being meet-closed Subset of L holds S1 /\ S2 is meet-closed
proofend;

theorem Th35: :: WAYBEL23:35
for L being sup-Semilattice
for x being Element of L holds downarrow x is join-closed
proofend;

theorem Th36: :: WAYBEL23:36
for L being Semilattice
for x being Element of L holds downarrow x is meet-closed
proofend;

theorem Th37: :: WAYBEL23:37
for L being sup-Semilattice
for x being Element of L holds uparrow x is join-closed
proofend;

theorem Th38: :: WAYBEL23:38
for L being Semilattice
for x being Element of L holds uparrow x is meet-closed
proofend;

registration
let L be sup-Semilattice;
let x be Element of L;
cluster downarrow x ->  join-closed ;
coherence
 downarrow x is join-closed by Th35;
cluster uparrow x ->  join-closed ;
coherence
 uparrow x is join-closed by Th37;
end;

registration
let L be Semilattice;
let x be Element of L;
cluster downarrow x ->  meet-closed ;
coherence
 downarrow x is meet-closed by Th36;
cluster uparrow x ->  meet-closed ;
coherence
 uparrow x is meet-closed by Th38;
end;

theorem Th39: :: WAYBEL23:39
for L being sup-Semilattice
for x being Element of L holds waybelow x is join-closed
proofend;

theorem Th40: :: WAYBEL23:40
for L being Semilattice
for x being Element of L holds waybelow x is meet-closed
proofend;

theorem Th41: :: WAYBEL23:41
for L being sup-Semilattice
for x being Element of L holds wayabove x is join-closed
proofend;

registration
let L be sup-Semilattice;
let x be Element of L;
cluster waybelow x ->  join-closed ;
coherence
 waybelow x is join-closed by Th39;
cluster wayabove x ->  join-closed ;
coherence
 wayabove x is join-closed by Th41;
end;

registration
let L be Semilattice;
let x be Element of L;
cluster waybelow x ->  meet-closed ;
coherence
 waybelow x is meet-closed by Th40;
end;

begin

definition
let T be TopStruct ;
func weight T ->  Cardinal equals :: WAYBEL23:def 5
 meet  {  (card B) where B is Basis of T : verum  }  ;
coherence
 meet  {  (card B) where B is Basis of T : verum  }  is Cardinal
proofend;
end;

:: deftheorem  defines weight WAYBEL23:def_5_:_
 for T being TopStruct holds weight T = meet  {  (card B) where B is Basis of T : verum  }  ;

definition
let T be TopStruct ;
attrT is second-countable  means :: WAYBEL23:def 6
 weight T c= omega ;
end;

:: deftheorem  defines second-countable WAYBEL23:def_6_:_
 for T being TopStruct holds
( T is second-countable iff weight T c= omega );

definition
let L be continuous sup-Semilattice;
mode CLbasis of L ->  Subset of L means :Def7: :: WAYBEL23:def 7
( it is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ it) ) );
existence
 ex b1 being Subset of L st
( b1 is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ b1) ) )
proofend;
end;

:: deftheorem Def7 defines CLbasis WAYBEL23:def_7_:_
 for L being continuous sup-Semilattice
for b2 being Subset of L holds
( b2 is CLbasis of L iff ( b2 is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ b2) ) ) );

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is with_bottom  means :Def8: :: WAYBEL23:def 8
 Bottom L in S;
end;

:: deftheorem Def8 defines with_bottom WAYBEL23:def_8_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is with_bottom iff Bottom L in S );

definition
let L be non empty RelStr ;
let S be Subset of L;
attrS is with_top  means :Def9: :: WAYBEL23:def 9
 Top L in S;
end;

:: deftheorem Def9 defines with_top WAYBEL23:def_9_:_
 for L being non empty RelStr
for S being Subset of L holds
( S is with_top iff Top L in S );

registration
let L be non empty RelStr ;
cluster with_bottom  ->  non empty for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is with_bottom holds
not b1 is empty by Def8;
end;

registration
let L be non empty RelStr ;
cluster with_top  ->  non empty for Element of K32( the carrier of L);
coherence
 for b1 being Subset of L st b1 is with_top holds
not b1 is empty by Def9;
end;

registration
let L be non empty RelStr ;
cluster with_bottom for Element of K32( the carrier of L);
existence
 ex b1 being Subset of L st b1 is with_bottom
proofend;
cluster with_top for Element of K32( the carrier of L);
existence
 ex b1 being Subset of L st b1 is with_top
proofend;
end;

registration
let L be continuous sup-Semilattice;
cluster with_bottom for CLbasis of L;
existence
 ex b1 being CLbasis of L st b1 is with_bottom
proofend;
cluster with_top for CLbasis of L;
existence
 ex b1 being CLbasis of L st b1 is with_top
proofend;
end;

theorem Th42: :: WAYBEL23:42
for L being non empty antisymmetric lower-bounded RelStr
for S being with_bottom Subset of L holds subrelstr S is lower-bounded
proofend;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
let S be with_bottom Subset of L;
cluster subrelstr S ->  lower-bounded ;
coherence
 subrelstr S is lower-bounded by Th42;
end;

registration
let L be continuous sup-Semilattice;
cluster  ->  join-closed for CLbasis of L;
coherence
 for b1 being CLbasis of L holds b1 is join-closed by Def7;
end;

registration
cluster non empty non trivial reflexive transitive antisymmetric upper-bounded bounded with_suprema with_infima up-complete satisfying_axiom_of_approximation continuous for RelStr ;
existence
 ex b1 being continuous LATTICE st
( b1 is bounded & not b1 is trivial )
proofend;
end;

registration
let L be non trivial lower-bounded continuous sup-Semilattice;
cluster  ->  non empty for CLbasis of L;
coherence
 for b1 being CLbasis of L holds not b1 is empty
proofend;
end;

theorem Th43: :: WAYBEL23:43
for L being sup-Semilattice holds the carrier of (CompactSublatt L) is join-closed Subset of L
proofend;

theorem Th44: :: WAYBEL23:44
for L being lower-bounded algebraic LATTICE holds the carrier of (CompactSublatt L) is with_bottom CLbasis of L
proofend;

theorem :: WAYBEL23:45
for L being lower-bounded continuous sup-Semilattice st the carrier of (CompactSublatt L) is CLbasis of L holds
L is algebraic
proofend;

theorem Th46: :: WAYBEL23:46
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L holds
( B is CLbasis of L iff for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B &amp; not b <= x &amp; b << y ) )
proofend;

theorem Th47: :: WAYBEL23:47
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B &amp; x <= b &amp; b << y ) )
proofend;

Lm2:  for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B &amp; ( for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B &amp; x <= b &amp; b << y ) ) holds
( the carrier of (CompactSublatt L) c= B &amp; ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B &amp; not b <= x &amp; b <= y ) ) )
proofend;

Lm3:  for L being lower-bounded continuous LATTICE
for B being Subset of L st ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B &amp; not b <= x &amp; b <= y ) ) holds
for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B &amp; not b <= x &amp; b << y )
proofend;

theorem Th48: :: WAYBEL23:48
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff ( the carrier of (CompactSublatt L) c= B &amp; ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B &amp; not b <= x &amp; b <= y ) ) ) )
proofend;

theorem :: WAYBEL23:49
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B &amp; not b <= x &amp; b <= y ) )
proofend;

theorem Th50: :: WAYBEL23:50
for L being lower-bounded sup-Semilattice
for S being non empty full SubRelStr of L st Bottom L in the carrier of S &amp; the carrier of S is join-closed Subset of L holds
for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S
proofend;

definition
let L be non empty reflexive transitive RelStr ;
let S be non empty full SubRelStr of L;
func supMap S ->  Function of (InclPoset (Ids S)),L means :Def10: :: WAYBEL23:def 10
 for I being Ideal of S holds it . I = "\/" (I,L);
existence
 ex b1 being Function of (InclPoset (Ids S)),L st
for I being Ideal of S holds b1 . I = "\/" (I,L)
proofend;
uniqueness
 for b1, b2 being Function of (InclPoset (Ids S)),L st ( for I being Ideal of S holds b1 . I = "\/" (I,L) ) &amp; ( for I being Ideal of S holds b2 . I = "\/" (I,L) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines supMap WAYBEL23:def_10_:_
 for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for b3 being Function of (InclPoset (Ids S)),L holds
( b3 = supMap S iff for I being Ideal of S holds b3 . I = "\/" (I,L) );

definition
let L be non empty reflexive transitive RelStr ;
let S be non empty full SubRelStr of L;
func idsMap S ->  Function of (InclPoset (Ids S)),(InclPoset (Ids L)) means :Def11: :: WAYBEL23:def 11
 for I being Ideal of S ex J being Subset of L st
( I = J &amp; it . I = downarrow J );
existence
 ex b1 being Function of (InclPoset (Ids S)),(InclPoset (Ids L)) st
for I being Ideal of S ex J being Subset of L st
( I = J &amp; b1 . I = downarrow J )
proofend;
uniqueness
 for b1, b2 being Function of (InclPoset (Ids S)),(InclPoset (Ids L)) st ( for I being Ideal of S ex J being Subset of L st
( I = J &amp; b1 . I = downarrow J ) ) &amp; ( for I being Ideal of S ex J being Subset of L st
( I = J &amp; b2 . I = downarrow J ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines idsMap WAYBEL23:def_11_:_
 for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for b3 being Function of (InclPoset (Ids S)),(InclPoset (Ids L)) holds
( b3 = idsMap S iff for I being Ideal of S ex J being Subset of L st
( I = J &amp; b3 . I = downarrow J ) );

registration
let L be reflexive RelStr ;
let B be Subset of L;
cluster subrelstr B ->  reflexive ;
coherence
 subrelstr B is reflexive ;
end;

registration
let L be transitive RelStr ;
let B be Subset of L;
cluster subrelstr B ->  transitive ;
coherence
 subrelstr B is transitive ;
end;

registration
let L be antisymmetric RelStr ;
let B be Subset of L;
cluster subrelstr B ->  antisymmetric ;
coherence
 subrelstr B is antisymmetric ;
end;

definition
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
func baseMap B ->  Function of L,(InclPoset (Ids (subrelstr B))) means :Def12: :: WAYBEL23:def 12
 for x being Element of L holds it . x = (waybelow x) /\ B;
existence
 ex b1 being Function of L,(InclPoset (Ids (subrelstr B))) st
for x being Element of L holds b1 . x = (waybelow x) /\ B
proofend;
uniqueness
 for b1, b2 being Function of L,(InclPoset (Ids (subrelstr B))) st ( for x being Element of L holds b1 . x = (waybelow x) /\ B ) &amp; ( for x being Element of L holds b2 . x = (waybelow x) /\ B ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines baseMap WAYBEL23:def_12_:_
 for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L
for b3 being Function of L,(InclPoset (Ids (subrelstr B))) holds
( b3 = baseMap B iff for x being Element of L holds b3 . x = (waybelow x) /\ B );

theorem Th51: :: WAYBEL23:51
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L holds
( dom (supMap S) = Ids S &amp; rng (supMap S) is Subset of L )
proofend;

theorem Th52: :: WAYBEL23:52
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for x being set holds
( x in dom (supMap S) iff x is Ideal of S )
proofend;

theorem Th53: :: WAYBEL23:53
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L holds
( dom (idsMap S) = Ids S &amp; rng (idsMap S) is Subset of (Ids L) )
proofend;

theorem Th54: :: WAYBEL23:54
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for x being set holds
( x in dom (idsMap S) iff x is Ideal of S )
proofend;

theorem Th55: :: WAYBEL23:55
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for x being set st x in rng (idsMap S) holds
x is Ideal of L
proofend;

theorem :: WAYBEL23:56
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds
( dom (baseMap B) = the carrier of L &amp; rng (baseMap B) is Subset of (Ids (subrelstr B)) ) by FUNCT_2:def_1, YELLOW_1:1;

theorem :: WAYBEL23:57
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L
for x being set st x in rng (baseMap B) holds
x is Ideal of (subrelstr B)
proofend;

theorem Th58: :: WAYBEL23:58
for L being non empty up-complete Poset
for S being non empty full SubRelStr of L holds supMap S is monotone
proofend;

theorem Th59: :: WAYBEL23:59
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L holds idsMap S is monotone
proofend;

theorem Th60: :: WAYBEL23:60
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds baseMap B is monotone
proofend;

registration
let L be non empty up-complete Poset;
let S be non empty full SubRelStr of L;
cluster supMap S ->  monotone ;
coherence
 supMap S is monotone by Th58;
end;

registration
let L be non empty reflexive transitive RelStr ;
let S be non empty full SubRelStr of L;
cluster idsMap S ->  monotone ;
coherence
 idsMap S is monotone by Th59;
end;

registration
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
cluster baseMap B ->  monotone ;
coherence
 baseMap B is monotone by Th60;
end;

theorem Th61: :: WAYBEL23:61
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds idsMap (subrelstr B) is sups-preserving
proofend;

theorem Th62: :: WAYBEL23:62
for L being non empty up-complete Poset
for S being non empty full SubRelStr of L holds supMap S = (SupMap L) * (idsMap S)
proofend;

theorem Th63: :: WAYBEL23:63
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds [(supMap (subrelstr B)),(baseMap B)] is Galois
proofend;

theorem Th64: :: WAYBEL23:64
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds
( supMap (subrelstr B) is upper_adjoint &amp; baseMap B is lower_adjoint )
proofend;

theorem Th65: :: WAYBEL23:65
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds rng (supMap (subrelstr B)) = the carrier of L
proofend;

theorem Th66: :: WAYBEL23:66
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds
( supMap (subrelstr B) is infs-preserving &amp; supMap (subrelstr B) is sups-preserving )
proofend;

theorem :: WAYBEL23:67
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds baseMap B is sups-preserving by Th64, WAYBEL_1:13;

registration
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
cluster supMap (subrelstr B) ->  infs-preserving sups-preserving ;
coherence
 ( supMap (subrelstr B) is infs-preserving &amp; supMap (subrelstr B) is sups-preserving ) by Th66;
cluster baseMap B ->  sups-preserving ;
coherence
 baseMap B is sups-preserving by Th64, WAYBEL_1:13;
end;

theorem Th68: :: WAYBEL23:68
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) =  {  (downarrow b) where b is Element of (subrelstr B) : verum  }
proofend;

theorem :: WAYBEL23:69
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic
proofend;

Lm4:  for L being lower-bounded continuous LATTICE st L is algebraic holds
( the carrier of (CompactSublatt L) is with_bottom CLbasis of L &amp; ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) )
proofend;

theorem Th70: :: WAYBEL23:70
for L being lower-bounded continuous LATTICE
for B being with_bottom CLbasis of L st ( for B1 being with_bottom CLbasis of L holds B c= B1 ) holds
for J being Element of (InclPoset (Ids (subrelstr B))) holds J = (waybelow ("\/" (J,L))) /\ B
proofend;

Lm5:  for L being lower-bounded continuous LATTICE st ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 holds
L is algebraic
proofend;

theorem :: WAYBEL23:71
for L being lower-bounded continuous LATTICE holds
( L is algebraic iff ( the carrier of (CompactSublatt L) is with_bottom CLbasis of L &amp; ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) ) ) by Lm4, Lm5;

theorem :: WAYBEL23:72
for L being lower-bounded continuous LATTICE holds
( L is algebraic iff ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 )
proofend;

theorem :: WAYBEL23:73
for T being TopStruct
for b being Basis of T holds weight T c= card b
proofend;

theorem :: WAYBEL23:74
for T being TopStruct ex b being Basis of T st card b = weight T
proofend;