:: WAYBEL23 semantic presentation

theorem Th1: :: WAYBEL23:1

for b₁ being non empty Poset
for b₂ being Element of b₁ holds compactbelow b₂ = (waybelow b₂) /\ the carrier of (CompactSublatt b₁)

proof end;

definition

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be Subset of (InclPoset (Ids c₁));
redefine func union as union c₂ -> Subset of a₁;
coherence

proof end;

end;

Lemma2: for b₁ being non empty set
for b₂ being Subset of (InclPoset b₁) st ex_sup_of b₂, InclPoset b₁ holds
union b₂ c= sup b₂

proof end;

theorem Th2: :: WAYBEL23:2

for b₁ being non empty RelStr
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
finsups b₂ c= finsups b₃

proof end;

theorem Th3: :: WAYBEL23:3

for b₁ being non empty transitive RelStr
for b₂ being non empty full sups-inheriting SubRelStr of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
finsups b₃ c= finsups b₄

proof end;

theorem Th4: :: WAYBEL23:4

for b₁ being non empty transitive antisymmetric complete RelStr
for b₂ being non empty full sups-inheriting SubRelStr of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
finsups b₃ = finsups b₄

proof end;

theorem Th5: :: WAYBEL23:5

for b₁ being complete sup-Semilattice
for b₂ being non empty full join-inheriting SubRelStr of b₁ st Bottom b₁ in the carrier of b₂ holds
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
finsups b₄ c= finsups b₃

proof end;

theorem Th6: :: WAYBEL23:6

for b₁ being lower-bounded sup-Semilattice
for b₂ being Subset of (InclPoset (Ids b₁)) holds sup b₂ = downarrow (finsups (union b₂))

proof end;

theorem Th7: :: WAYBEL23:7

for b₁ being reflexive transitive RelStr
for b₂ being Subset of b₁ holds downarrow (downarrow b₂) = downarrow b₂

proof end;

theorem Th8: :: WAYBEL23:8

for b₁ being reflexive transitive RelStr
for b₂ being Subset of b₁ holds uparrow (uparrow b₂) = uparrow b₂

proof end;

theorem Th9: :: WAYBEL23:9

for b₁ being non empty reflexive transitive RelStr
for b₂ being Element of b₁ holds downarrow (downarrow b₂) = downarrow b₂

proof end;

theorem Th10: :: WAYBEL23:10

for b₁ being non empty reflexive transitive RelStr
for b₂ being Element of b₁ holds uparrow (uparrow b₂) = uparrow b₂

proof end;

theorem Th11: :: WAYBEL23:11

for b₁ being non empty RelStr
for b₂ being non empty SubRelStr of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
downarrow b₄ c= downarrow b₃

proof end;

theorem Th12: :: WAYBEL23:12

for b₁ being non empty RelStr
for b₂ being non empty SubRelStr of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
uparrow b₄ c= uparrow b₃

proof end;

theorem Th13: :: WAYBEL23:13

for b₁ being non empty RelStr
for b₂ being non empty SubRelStr of b₁
for b₃ being Element of b₁
for b₄ being Element of b₂ st b₃ = b₄ holds
downarrow b₄ c= downarrow b₃

proof end;

theorem Th14: :: WAYBEL23:14

for b₁ being non empty RelStr
for b₂ being non empty SubRelStr of b₁
for b₃ being Element of b₁
for b₄ being Element of b₂ st b₃ = b₄ holds
uparrow b₄ c= uparrow b₃

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
attr a₂ is meet-closed means :Def1: :: WAYBEL23:def 1
subrelstr a₂ is meet-inheriting;

end;

:: deftheorem Def1 defines meet-closed WAYBEL23:def 1 :

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
attr a₂ is join-closed means :Def2: :: WAYBEL23:def 2
subrelstr a₂ is join-inheriting;

end;

:: deftheorem Def2 defines join-closed WAYBEL23:def 2 :

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
attr a₂ is infs-closed means :Def3: :: WAYBEL23:def 3
subrelstr a₂ is infs-inheriting;

end;

:: deftheorem Def3 defines infs-closed WAYBEL23:def 3 :

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
attr a₂ is sups-closed means :Def4: :: WAYBEL23:def 4
subrelstr a₂ is sups-inheriting;

end;

:: deftheorem Def4 defines sups-closed WAYBEL23:def 4 :

registration

let c₁ be non empty RelStr ;
cluster infs-closed -> meet-closed Element of K10(the carrier of a₁);
coherence

proof end;

cluster sups-closed -> join-closed Element of K10(the carrier of a₁);
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster non empty meet-closed join-closed infs-closed sups-closed Element of K10(the carrier of a₁);
existence

proof end;

end;

theorem Th15: :: WAYBEL23:15

for b₁ being non empty RelStr
for b₂ being Subset of b₁ holds
( b₂ is meet-closed iff for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ & ex_inf_of {b₃,b₄},b₁ holds
inf {b₃,b₄} in b₂ )

proof end;

theorem Th16: :: WAYBEL23:16

for b₁ being non empty RelStr
for b₂ being Subset of b₁ holds
( b₂ is join-closed iff for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ & ex_sup_of {b₃,b₄},b₁ holds
sup {b₃,b₄} in b₂ )

proof end;

theorem Th17: :: WAYBEL23:17

for b₁ being antisymmetric with_infima RelStr
for b₂ being Subset of b₁ holds
( b₂ is meet-closed iff for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ holds
inf {b₃,b₄} in b₂ )

proof end;

theorem Th18: :: WAYBEL23:18

for b₁ being antisymmetric with_suprema RelStr
for b₂ being Subset of b₁ holds
( b₂ is join-closed iff for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ holds
sup {b₃,b₄} in b₂ )

proof end;

theorem Th19: :: WAYBEL23:19

for b₁ being non empty RelStr
for b₂ being Subset of b₁ holds
( b₂ is infs-closed iff for b₃ being Subset of b₂ st ex_inf_of b₃,b₁ holds
"/\" b₃,b₁ in b₂ )

proof end;

theorem Th20: :: WAYBEL23:20

for b₁ being non empty RelStr
for b₂ being Subset of b₁ holds
( b₂ is sups-closed iff for b₃ being Subset of b₂ st ex_sup_of b₃,b₁ holds
"\/" b₃,b₁ in b₂ )

proof end;

theorem Th21: :: WAYBEL23:21

for b₁ being non empty transitive RelStr
for b₂ being non empty infs-closed Subset of b₁
for b₃ being Subset of b₂ st ex_inf_of b₃,b₁ holds
( ex_inf_of b₃, subrelstr b₂ & "/\" b₃,(subrelstr b₂) = "/\" b₃,b₁ )

proof end;

theorem Th22: :: WAYBEL23:22

for b₁ being non empty transitive RelStr
for b₂ being non empty sups-closed Subset of b₁
for b₃ being Subset of b₂ st ex_sup_of b₃,b₁ holds
( ex_sup_of b₃, subrelstr b₂ & "\/" b₃,(subrelstr b₂) = "\/" b₃,b₁ )

proof end;

theorem Th23: :: WAYBEL23:23

for b₁ being non empty transitive RelStr
for b₂ being non empty meet-closed Subset of b₁
for b₃, b₄ being Element of b₂ st ex_inf_of {b₃,b₄},b₁ holds
( ex_inf_of {b₃,b₄}, subrelstr b₂ & "/\" {b₃,b₄},(subrelstr b₂) = "/\" {b₃,b₄},b₁ )

proof end;

theorem Th24: :: WAYBEL23:24

for b₁ being non empty transitive RelStr
for b₂ being non empty join-closed Subset of b₁
for b₃, b₄ being Element of b₂ st ex_sup_of {b₃,b₄},b₁ holds
( ex_sup_of {b₃,b₄}, subrelstr b₂ & "\/" {b₃,b₄},(subrelstr b₂) = "\/" {b₃,b₄},b₁ )

proof end;

theorem Th25: :: WAYBEL23:25

for b₁ being transitive antisymmetric with_infima RelStr
for b₂ being non empty meet-closed Subset of b₁ holds subrelstr b₂ is with_infima

proof end;

theorem Th26: :: WAYBEL23:26

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂ being non empty join-closed Subset of b₁ holds subrelstr b₂ is with_suprema

proof end;

registration

let c₁ be transitive antisymmetric with_infima RelStr ;
let c₂ be non empty meet-closed Subset of c₁;
cluster subrelstr a₂ -> with_infima ;
coherence by Th25;

end;

registration

let c₁ be transitive antisymmetric with_suprema RelStr ;
let c₂ be non empty join-closed Subset of c₁;
cluster subrelstr a₂ -> with_suprema ;
coherence by Th26;

end;

theorem Th27: :: WAYBEL23:27

for b₁ being non empty transitive antisymmetric complete RelStr
for b₂ being non empty infs-closed Subset of b₁
for b₃ being Subset of b₂ holds "/\" b₃,(subrelstr b₂) = "/\" b₃,b₁

proof end;

theorem Th28: :: WAYBEL23:28

for b₁ being non empty transitive antisymmetric complete RelStr
for b₂ being non empty sups-closed Subset of b₁
for b₃ being Subset of b₂ holds "\/" b₃,(subrelstr b₂) = "\/" b₃,b₁

proof end;

theorem Th29: :: WAYBEL23:29

for b₁ being Semilattice
for b₂ being meet-closed Subset of b₁ holds b₂ is filtered

proof end;

theorem Th30: :: WAYBEL23:30

for b₁ being sup-Semilattice
for b₂ being join-closed Subset of b₁ holds b₂ is directed

proof end;

registration

let c₁ be Semilattice;
cluster meet-closed -> filtered Element of K10(the carrier of a₁);
coherence by Th29;

end;

registration

let c₁ be sup-Semilattice;
cluster join-closed -> directed Element of K10(the carrier of a₁);
coherence by Th30;

end;

theorem Th31: :: WAYBEL23:31

for b₁ being Semilattice
for b₂ being non empty upper Subset of b₁ holds
( b₂ is Filter of b₁ iff b₂ is meet-closed )

proof end;

theorem Th32: :: WAYBEL23:32

for b₁ being sup-Semilattice
for b₂ being non empty lower Subset of b₁ holds
( b₂ is Ideal of b₁ iff b₂ is join-closed )

proof end;

theorem Th33: :: WAYBEL23:33

for b₁ being non empty RelStr
for b₂, b₃ being join-closed Subset of b₁ holds b₂ /\ b₃ is join-closed

proof end;

theorem Th34: :: WAYBEL23:34

for b₁ being non empty RelStr
for b₂, b₃ being meet-closed Subset of b₁ holds b₂ /\ b₃ is meet-closed

proof end;

theorem Th35: :: WAYBEL23:35

for b₁ being sup-Semilattice
for b₂ being Element of b₁ holds downarrow b₂ is join-closed

proof end;

theorem Th36: :: WAYBEL23:36

for b₁ being Semilattice
for b₂ being Element of b₁ holds downarrow b₂ is meet-closed

proof end;

theorem Th37: :: WAYBEL23:37

for b₁ being sup-Semilattice
for b₂ being Element of b₁ holds uparrow b₂ is join-closed

proof end;

theorem Th38: :: WAYBEL23:38

for b₁ being Semilattice
for b₂ being Element of b₁ holds uparrow b₂ is meet-closed

proof end;

registration

let c₁ be sup-Semilattice;
let c₂ be Element of c₁;
cluster downarrow a₂ -> join-closed ;
coherence by Th35;
cluster uparrow a₂ -> directed join-closed ;
coherence by Th37;

end;

registration

let c₁ be Semilattice;
let c₂ be Element of c₁;
cluster downarrow a₂ -> filtered meet-closed ;
coherence by Th36;
cluster uparrow a₂ -> meet-closed ;
coherence by Th38;

end;

theorem Th39: :: WAYBEL23:39

for b₁ being sup-Semilattice
for b₂ being Element of b₁ holds waybelow b₂ is join-closed

proof end;

theorem Th40: :: WAYBEL23:40

for b₁ being Semilattice
for b₂ being Element of b₁ holds waybelow b₂ is meet-closed

proof end;

theorem Th41: :: WAYBEL23:41

for b₁ being sup-Semilattice
for b₂ being Element of b₁ holds wayabove b₂ is join-closed

proof end;

registration

let c₁ be sup-Semilattice;
let c₂ be Element of c₁;
cluster waybelow a₂ -> join-closed ;
coherence by Th39;
cluster wayabove a₂ -> directed join-closed ;
coherence by Th41;

end;

registration

let c₁ be Semilattice;
let c₂ be Element of c₁;
cluster waybelow a₂ -> filtered meet-closed ;
coherence by Th40;

end;

definition

let c₁ be TopStruct ;
func weight c₁ -> Cardinal equals :: WAYBEL23:def 5
meet { (Card b₁) where B is Basis of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def5 defines weight WAYBEL23:def 5 :

definition

let c₁ be TopStruct ;
attr a₁ is second-countable means :: WAYBEL23:def 6
weight a₁ c= omega ;

end;

:: deftheorem Def6 defines second-countable WAYBEL23:def 6 :

definition

let c₁ be continuous sup-Semilattice;
mode CLbasis of c₁ -> Subset of a₁ means :Def7: :: WAYBEL23:def 7
( a₂ is join-closed & ( for b₁ being Element of a₁ holds b₁ = sup ((waybelow b₁) /\ a₂) ) );
existence

proof end;

end;

:: deftheorem Def7 defines CLbasis WAYBEL23:def 7 :

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
attr a₂ is with_bottom means :Def8: :: WAYBEL23:def 8
Bottom a₁ in a₂;

end;

:: deftheorem Def8 defines with_bottom WAYBEL23:def 8 :

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
attr a₂ is with_top means :Def9: :: WAYBEL23:def 9
Top a₁ in a₂;

end;

:: deftheorem Def9 defines with_top WAYBEL23:def 9 :

registration

let c₁ be non empty RelStr ;
cluster with_bottom -> non empty Element of K10(the carrier of a₁);
coherence by Def8;

end;

registration

let c₁ be non empty RelStr ;
cluster with_top -> non empty Element of K10(the carrier of a₁);
coherence by Def9;

end;

registration

let c₁ be non empty RelStr ;
cluster non empty with_bottom Element of K10(the carrier of a₁);
existence

proof end;

cluster non empty with_top Element of K10(the carrier of a₁);
existence

proof end;

end;

registration

let c₁ be continuous sup-Semilattice;
cluster non empty with_bottom CLbasis of a₁;
existence

proof end;

cluster non empty with_top CLbasis of a₁;
existence

proof end;

end;

theorem Th42: :: WAYBEL23:42

for b₁ being non empty antisymmetric lower-bounded RelStr
for b₂ being with_bottom Subset of b₁ holds subrelstr b₂ is lower-bounded

proof end;

registration

let c₁ be non empty antisymmetric lower-bounded RelStr ;
let c₂ be with_bottom Subset of c₁;
cluster subrelstr a₂ -> lower-bounded ;
coherence by Th42;

end;

registration

let c₁ be continuous sup-Semilattice;
cluster -> directed join-closed CLbasis of a₁;
coherence by Def7;

end;

registration

cluster bounded continuous non trivial RelStr ;
existence

proof end;

end;

registration

let c₁ be lower-bounded continuous non trivial sup-Semilattice;
cluster -> non empty directed join-closed CLbasis of a₁;
coherence

proof end;

end;

theorem Th43: :: WAYBEL23:43

for b₁ being sup-Semilattice holds the carrier of (CompactSublatt b₁) is join-closed Subset of b₁

proof end;

theorem Th44: :: WAYBEL23:44

for b₁ being lower-bounded algebraic LATTICE holds the carrier of (CompactSublatt b₁) is with_bottom CLbasis of b₁

proof end;

theorem Th45: :: WAYBEL23:45

for b₁ being lower-bounded continuous sup-Semilattice st the carrier of (CompactSublatt b₁) is CLbasis of b₁ holds
b₁ is algebraic

proof end;

theorem Th46: :: WAYBEL23:46

for b₁ being lower-bounded continuous LATTICE
for b₂ being join-closed Subset of b₁ holds
( b₂ is CLbasis of b₁ iff for b₃, b₄ being Element of b₁ st not b₄ <= b₃ holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & not b₅ <= b₃ & b₅ << b₄ ) )

proof end;

theorem Th47: :: WAYBEL23:47

for b₁ being lower-bounded continuous LATTICE
for b₂ being join-closed Subset of b₁ st Bottom b₁ in b₂ holds
( b₂ is CLbasis of b₁ iff for b₃, b₄ being Element of b₁ st b₃ << b₄ holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & b₃ <= b₅ & b₅ << b₄ ) )

proof end;

Lemma39: for b₁ being lower-bounded continuous LATTICE
for b₂ being join-closed Subset of b₁ st Bottom b₁ in b₂ & ( for b₃, b₄ being Element of b₁ st b₃ << b₄ holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & b₃ <= b₅ & b₅ << b₄ ) ) holds
( the carrier of (CompactSublatt b₁) c= b₂ & ( for b₃, b₄ being Element of b₁ st not b₄ <= b₃ holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & not b₅ <= b₃ & b₅ <= b₄ ) ) )

proof end;

Lemma40: for b₁ being lower-bounded continuous LATTICE
for b₂ being Subset of b₁ st ( for b₃, b₄ being Element of b₁ st not b₄ <= b₃ holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & not b₅ <= b₃ & b₅ <= b₄ ) ) holds
for b₃, b₄ being Element of b₁ st not b₄ <= b₃ holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & not b₅ <= b₃ & b₅ << b₄ )

proof end;

theorem Th48: :: WAYBEL23:48

for b₁ being lower-bounded continuous LATTICE
for b₂ being join-closed Subset of b₁ st Bottom b₁ in b₂ holds
( b₂ is CLbasis of b₁ iff ( the carrier of (CompactSublatt b₁) c= b₂ & ( for b₃, b₄ being Element of b₁ st not b₄ <= b₃ holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & not b₅ <= b₃ & b₅ <= b₄ ) ) ) )

proof end;

theorem Th49: :: WAYBEL23:49

for b₁ being lower-bounded continuous LATTICE
for b₂ being join-closed Subset of b₁ st Bottom b₁ in b₂ holds
( b₂ is CLbasis of b₁ iff for b₃, b₄ being Element of b₁ st not b₄ <= b₃ holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & not b₅ <= b₃ & b₅ <= b₄ ) )

proof end;

theorem Th50: :: WAYBEL23:50

for b₁ being lower-bounded sup-Semilattice
for b₂ being non empty full SubRelStr of b₁ st Bottom b₁ in the carrier of b₂ & the carrier of b₂ is join-closed Subset of b₁ holds
for b₃ being Element of b₁ holds (waybelow b₃) /\ the carrier of b₂ is Ideal of b₂

proof end;

definition

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be non empty full SubRelStr of c₁;
func supMap c₂ -> Function of (InclPoset (Ids a₂)),a₁ means :Def10: :: WAYBEL23:def 10
for b₁ being Ideal of a₂ holds a₃ . b₁ = "\/" b₁,a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines supMap WAYBEL23:def 10 :

definition

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be non empty full SubRelStr of c₁;
func idsMap c₂ -> Function of (InclPoset (Ids a₂)),(InclPoset (Ids a₁)) means :Def11: :: WAYBEL23:def 11
for b₁ being Ideal of a₂ ex b₂ being Subset of a₁ st
( b₁ = b₂ & a₃ . b₁ = downarrow b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines idsMap WAYBEL23:def 11 :

registration

let c₁ be reflexive RelStr ;
let c₂ be Subset of c₁;
cluster subrelstr a₂ -> reflexive ;
coherence ;

end;

registration

let c₁ be transitive RelStr ;
let c₂ be Subset of c₁;
cluster subrelstr a₂ -> transitive ;
coherence ;

end;

registration

let c₁ be antisymmetric RelStr ;
let c₂ be Subset of c₁;
cluster subrelstr a₂ -> antisymmetric ;
coherence ;

end;

definition

let c₁ be lower-bounded continuous sup-Semilattice;
let c₂ be with_bottom CLbasis of c₁;
func baseMap c₂ -> Function of a₁,(InclPoset (Ids (subrelstr a₂))) means :Def12: :: WAYBEL23:def 12
for b₁ being Element of a₁ holds a₃ . b₁ = (waybelow b₁) /\ a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines baseMap WAYBEL23:def 12 :

theorem Th51: :: WAYBEL23:51

for b₁ being non empty reflexive transitive RelStr
for b₂ being non empty full SubRelStr of b₁ holds
( dom (supMap b₂) = Ids b₂ & rng (supMap b₂) is Subset of b₁ )

proof end;

theorem Th52: :: WAYBEL23:52

for b₁ being non empty reflexive transitive RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃ being set holds
( b₃ in dom (supMap b₂) iff b₃ is Ideal of b₂ )

proof end;

theorem Th53: :: WAYBEL23:53

for b₁ being non empty reflexive transitive RelStr
for b₂ being non empty full SubRelStr of b₁ holds
( dom (idsMap b₂) = Ids b₂ & rng (idsMap b₂) is Subset of (Ids b₁) )

proof end;

theorem Th54: :: WAYBEL23:54

for b₁ being non empty reflexive transitive RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃ being set holds
( b₃ in dom (idsMap b₂) iff b₃ is Ideal of b₂ )

proof end;

theorem Th55: :: WAYBEL23:55

for b₁ being non empty reflexive transitive RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃ being set st b₃ in rng (idsMap b₂) holds
b₃ is Ideal of b₁

proof end;

theorem Th56: :: WAYBEL23:56

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds
( dom (baseMap b₂) = the carrier of b₁ & rng (baseMap b₂) is Subset of (Ids (subrelstr b₂)) ) by FUNCT_2:def 1, YELLOW_1:1;

theorem Th57: :: WAYBEL23:57

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁
for b₃ being set st b₃ in rng (baseMap b₂) holds
b₃ is Ideal of (subrelstr b₂)

proof end;

theorem Th58: :: WAYBEL23:58

for b₁ being non empty up-complete Poset
for b₂ being non empty full SubRelStr of b₁ holds supMap b₂ is monotone

proof end;

theorem Th59: :: WAYBEL23:59

for b₁ being non empty reflexive transitive RelStr
for b₂ being non empty full SubRelStr of b₁ holds idsMap b₂ is monotone

proof end;

theorem Th60: :: WAYBEL23:60

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds baseMap b₂ is monotone

proof end;

registration

let c₁ be non empty up-complete Poset;
let c₂ be non empty full SubRelStr of c₁;
cluster supMap a₂ -> monotone ;
coherence by Th58;

end;

registration

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be non empty full SubRelStr of c₁;
cluster idsMap a₂ -> monotone ;
coherence by Th59;

end;

registration

let c₁ be lower-bounded continuous sup-Semilattice;
let c₂ be with_bottom CLbasis of c₁;
cluster baseMap a₂ -> monotone ;
coherence by Th60;

end;

theorem Th61: :: WAYBEL23:61

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds idsMap (subrelstr b₂) is sups-preserving

proof end;

theorem Th62: :: WAYBEL23:62

for b₁ being non empty up-complete Poset
for b₂ being non empty full SubRelStr of b₁ holds supMap b₂ = (SupMap b₁) * (idsMap b₂)

proof end;

theorem Th63: :: WAYBEL23:63

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds [(supMap (subrelstr b₂)),(baseMap b₂)] is Galois

proof end;

theorem Th64: :: WAYBEL23:64

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds
( supMap (subrelstr b₂) is upper_adjoint & baseMap b₂ is lower_adjoint )

proof end;

theorem Th65: :: WAYBEL23:65

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds rng (supMap (subrelstr b₂)) = the carrier of b₁

proof end;

theorem Th66: :: WAYBEL23:66

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds
( supMap (subrelstr b₂) is infs-preserving & supMap (subrelstr b₂) is sups-preserving )

proof end;

theorem Th67: :: WAYBEL23:67

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds baseMap b₂ is sups-preserving

proof end;

registration

let c₁ be lower-bounded continuous sup-Semilattice;
let c₂ be with_bottom CLbasis of c₁;
cluster supMap (subrelstr a₂) -> monotone infs-preserving sups-preserving ;
coherence by Th66;
cluster baseMap a₂ -> monotone sups-preserving ;
coherence by Th67;

end;

theorem Th68: :: WAYBEL23:68

canceled;

theorem Th69: :: WAYBEL23:69

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds the carrier of (CompactSublatt (InclPoset (Ids (subrelstr b₂)))) = { (downarrow b₃) where B is Element of (subrelstr b₂) : verum }

proof end;

theorem Th70: :: WAYBEL23:70

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds CompactSublatt (InclPoset (Ids (subrelstr b₂))), subrelstr b₂ are_isomorphic

proof end;

Lemma62: for b₁ being lower-bounded continuous LATTICE st b₁ is algebraic holds
( the carrier of (CompactSublatt b₁) is with_bottom CLbasis of b₁ & ( for b₂ being with_bottom CLbasis of b₁ holds the carrier of (CompactSublatt b₁) c= b₂ ) )

proof end;

theorem Th71: :: WAYBEL23:71

for b₁ being lower-bounded continuous LATTICE
for b₂ being with_bottom CLbasis of b₁ st ( for b₃ being with_bottom CLbasis of b₁ holds b₂ c= b₃ ) holds
for b₃ being Element of (InclPoset (Ids (subrelstr b₂))) holds b₃ = (waybelow ("\/" b₃,b₁)) /\ b₂

proof end;

Lemma64: for b₁ being lower-bounded continuous LATTICE st ex b₂ being with_bottom CLbasis of b₁ st
for b₃ being with_bottom CLbasis of b₁ holds b₂ c= b₃ holds
b₁ is algebraic

proof end;

theorem Th72: :: WAYBEL23:72

for b₁ being lower-bounded continuous LATTICE holds
( b₁ is algebraic iff ( the carrier of (CompactSublatt b₁) is with_bottom CLbasis of b₁ & ( for b₂ being with_bottom CLbasis of b₁ holds the carrier of (CompactSublatt b₁) c= b₂ ) ) ) by Lemma62, Lemma64;

theorem Th73: :: WAYBEL23:73

for b₁ being lower-bounded continuous LATTICE holds
( b₁ is algebraic iff ex b₂ being with_bottom CLbasis of b₁ st
for b₃ being with_bottom CLbasis of b₁ holds b₂ c= b₃ )

proof end;