:: WAYBEL13 semantic presentation

theorem Th1: :: WAYBEL13:1

for b₁ being non empty reflexive transitive RelStr
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
compactbelow b₂ c= compactbelow b₃

proof end;

theorem Th2: :: WAYBEL13:2

for b₁ being non empty reflexive RelStr
for b₂ being Element of b₁ holds compactbelow b₂ is Subset of (CompactSublatt b₁)

proof end;

theorem Th3: :: WAYBEL13:3

for b₁ being RelStr
for b₂ being SubRelStr of b₁
for b₃ being Subset of b₂ holds b₃ is Subset of b₁

proof end;

theorem Th4: :: WAYBEL13:4

for b₁ being non empty reflexive transitive with_suprema RelStr holds the carrier of b₁ is Ideal of b₁

proof end;

theorem Th5: :: WAYBEL13:5

for b₁ being non empty reflexive antisymmetric lower-bounded RelStr
for b₂ being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is up-complete holds
the carrier of (CompactSublatt b₁) = the carrier of (CompactSublatt b₂)

proof end;

theorem Th6: :: WAYBEL13:6

for b₁ being lower-bounded algebraic LATTICE
for b₂ being CLSubFrame of b₁ holds b₂ is algebraic

proof end;

theorem Th7: :: WAYBEL13:7

for b₁, b₂ being set
for b₃ being CLSubFrame of BoolePoset b₁ holds
( b₂ in the carrier of (CompactSublatt b₃) iff ex b₄ being Element of (BoolePoset b₁) st
( b₄ is finite & b₂ = meet { b₅ where B is Element of b₃ : b₄ c= b₅ } & b₄ c= b₂ ) )

proof end;

theorem Th8: :: WAYBEL13:8

for b₁ being lower-bounded sup-Semilattice holds InclPoset (Ids b₁) is CLSubFrame of BoolePoset the carrier of b₁

proof end;

registration

let c₁ be non empty reflexive transitive RelStr ;
cluster principal Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th9: :: WAYBEL13:9

for b₁ being lower-bounded sup-Semilattice
for b₂ being non empty directed Subset of (InclPoset (Ids b₁)) holds sup b₂ = union b₂

proof end;

theorem Th10: :: WAYBEL13:10

for b₁ being lower-bounded sup-Semilattice holds InclPoset (Ids b₁) is algebraic

proof end;

theorem Th11: :: WAYBEL13:11

for b₁ being lower-bounded sup-Semilattice
for b₂ being Element of (InclPoset (Ids b₁)) holds
( b₂ is compact iff b₂ is principal Ideal of b₁ )

proof end;

theorem Th12: :: WAYBEL13:12

for b₁ being lower-bounded sup-Semilattice
for b₂ being Element of (InclPoset (Ids b₁)) holds
( b₂ is compact iff ex b₃ being Element of b₁ st b₂ = downarrow b₃ )

proof end;

theorem Th13: :: WAYBEL13:13

for b₁ being lower-bounded sup-Semilattice
for b₂ being Function of b₁,(CompactSublatt (InclPoset (Ids b₁))) st ( for b₃ being Element of b₁ holds b₂ . b₃ = downarrow b₃ ) holds
b₂ is isomorphic

proof end;

theorem Th14: :: WAYBEL13:14

for b₁ being lower-bounded LATTICE holds InclPoset (Ids b₁) is arithmetic

proof end;

theorem Th15: :: WAYBEL13:15

for b₁ being lower-bounded sup-Semilattice holds CompactSublatt b₁ is lower-bounded sup-Semilattice

proof end;

theorem Th16: :: WAYBEL13:16

for b₁ being lower-bounded algebraic sup-Semilattice
for b₂ being Function of b₁,(InclPoset (Ids (CompactSublatt b₁))) st ( for b₃ being Element of b₁ holds b₂ . b₃ = compactbelow b₃ ) holds
b₂ is isomorphic

proof end;

theorem Th17: :: WAYBEL13:17

for b₁ being lower-bounded algebraic sup-Semilattice
for b₂ being Element of b₁ holds
( compactbelow b₂ is principal Ideal of (CompactSublatt b₁) iff b₂ is compact )

proof end;

theorem Th18: :: WAYBEL13:18

for b₁, b₂ being non empty RelStr
for b₃ being Subset of b₁
for b₄ being Element of b₁
for b₅ being Function of b₁,b₂ st b₅ is isomorphic holds
( b₄ is_<=_than b₃ iff b₅ . b₄ is_<=_than b₅ .: b₃ )

proof end;

theorem Th19: :: WAYBEL13:19

for b₁, b₂ being non empty RelStr
for b₃ being Subset of b₁
for b₄ being Element of b₁
for b₅ being Function of b₁,b₂ st b₅ is isomorphic holds
( b₄ is_>=_than b₃ iff b₅ . b₄ is_>=_than b₅ .: b₃ )

proof end;

theorem Th20: :: WAYBEL13:20

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being Function of b₁,b₂ st b₃ is isomorphic holds
( b₃ is infs-preserving & b₃ is sups-preserving )

proof end;

registration

let c₁, c₂ be non empty antisymmetric RelStr ;
cluster isomorphic -> infs-preserving sups-preserving M4(the carrier of a₁,the carrier of a₂);
coherence by Th20;

end;

theorem Th21: :: WAYBEL13:21

for b₁, b₂, b₃ being non empty transitive antisymmetric RelStr
for b₄ being Function of b₁,b₂ st b₄ is infs-preserving & b₂ is full infs-inheriting SubRelStr of b₃ & b₃ is complete holds
ex b₅ being Function of b₁,b₃ st
( b₄ = b₅ & b₅ is infs-preserving )

proof end;

theorem Th22: :: WAYBEL13:22

for b₁, b₂, b₃ being non empty transitive antisymmetric RelStr
for b₄ being Function of b₁,b₂ st b₄ is monotone & b₄ is directed-sups-preserving & b₂ is full directed-sups-inheriting SubRelStr of b₃ & b₃ is complete holds
ex b₅ being Function of b₁,b₃ st
( b₄ = b₅ & b₅ is directed-sups-preserving )

proof end;

theorem Th23: :: WAYBEL13:23

for b₁ being lower-bounded sup-Semilattice holds InclPoset (Ids (CompactSublatt b₁)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt b₁)

proof end;

Lemma21: for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₃ is sups-preserving holds
b₃ is directed-sups-preserving

proof end;

theorem Th24: :: WAYBEL13:24

for b₁ being lower-bounded algebraic LATTICE ex b₂ being Function of b₁,(BoolePoset the carrier of (CompactSublatt b₁)) st
( b₂ is infs-preserving & b₂ is directed-sups-preserving & b₂ is one-to-one & ( for b₃ being Element of b₁ holds b₂ . b₃ = compactbelow b₃ ) )

proof end;

theorem Th25: :: WAYBEL13:25

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is lower-bounded algebraic LATTICE ) holds
product b₂ is lower-bounded algebraic LATTICE

proof end;

Lemma23: for b₁ being lower-bounded LATTICE st b₁ is algebraic holds
ex b₂ being non empty set ex b₃ being full SubRelStr of BoolePoset b₂ st
( b₃ is infs-inheriting & b₃ is directed-sups-inheriting & b₁,b₃ are_isomorphic )

proof end;

theorem Th26: :: WAYBEL13:26

for b₁, b₂ being non empty RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
b₁,b₂ are_isomorphic

proof end;

Lemma25: for b₁ being LATTICE st ex b₂ being non empty set ex b₃ being full SubRelStr of BoolePoset b₂ st
( b₃ is infs-inheriting & b₃ is directed-sups-inheriting & b₁,b₃ are_isomorphic ) holds
ex b₂ being non empty set ex b₃ being closure Function of (BoolePoset b₂),(BoolePoset b₂) st
( b₃ is directed-sups-preserving & b₁, Image b₃ are_isomorphic )

proof end;

Lemma26: for b₁ being LATTICE st ex b₂ being set ex b₃ being full SubRelStr of BoolePoset b₂ st
( b₃ is infs-inheriting & b₃ is directed-sups-inheriting & b₁,b₃ are_isomorphic ) holds
ex b₂ being set ex b₃ being closure Function of (BoolePoset b₂),(BoolePoset b₂) st
( b₃ is directed-sups-preserving & b₁, Image b₃ are_isomorphic )

proof end;

Lemma27: for b₁, b₂ being non empty up-complete Poset
for b₃ being Function of b₁,b₂ st b₃ is isomorphic holds
for b₄, b₅ being Element of b₁ st b₄ << b₅ holds
b₃ . b₄ << b₃ . b₅

proof end;

theorem Th27: :: WAYBEL13:27

for b₁, b₂ being non empty up-complete Poset
for b₃ being Function of b₁,b₂ st b₃ is isomorphic holds
for b₄, b₅ being Element of b₁ holds
( b₄ << b₅ iff b₃ . b₄ << b₃ . b₅ )

proof end;

theorem Th28: :: WAYBEL13:28

for b₁, b₂ being non empty up-complete Poset
for b₃ being Function of b₁,b₂ st b₃ is isomorphic holds
for b₄ being Element of b₁ holds
( b₄ is compact iff b₃ . b₄ is compact )

proof end;

theorem Th29: :: WAYBEL13:29

for b₁, b₂ being non empty up-complete Poset
for b₃ being Function of b₁,b₂ st b₃ is isomorphic holds
for b₄ being Element of b₁ holds b₃ .: (compactbelow b₄) = compactbelow (b₃ . b₄)

proof end;

theorem Th30: :: WAYBEL13:30

for b₁, b₂ being non empty Poset st b₁,b₂ are_isomorphic & b₁ is up-complete holds
b₂ is up-complete

proof end;

theorem Th31: :: WAYBEL13:31

for b₁, b₂ being non empty Poset st b₁,b₂ are_isomorphic & b₁ is complete & b₁ is satisfying_axiom_K holds
b₂ is satisfying_axiom_K

proof end;

theorem Th32: :: WAYBEL13:32

for b₁, b₂ being sup-Semilattice st b₁,b₂ are_isomorphic & b₁ is lower-bounded & b₁ is algebraic holds
b₂ is algebraic

proof end;

Lemma34: for b₁ being LATTICE st ex b₂ being set ex b₃ being closure Function of (BoolePoset b₂),(BoolePoset b₂) st
( b₃ is directed-sups-preserving & b₁, Image b₃ are_isomorphic ) holds
b₁ is algebraic

proof end;

theorem Th33: :: WAYBEL13:33

for b₁ being lower-bounded continuous sup-Semilattice holds
( SupMap b₁ is infs-preserving & SupMap b₁ is sups-preserving )

proof end;

theorem Th34: :: WAYBEL13:34

for b₁ being lower-bounded LATTICE holds
( ( b₁ is algebraic implies ex b₂ being non empty set ex b₃ being full SubRelStr of BoolePoset b₂ st
( b₃ is infs-inheriting & b₃ is directed-sups-inheriting & b₁,b₃ are_isomorphic ) ) & ( ex b₂ being set ex b₃ being full SubRelStr of BoolePoset b₂ st
( b₃ is infs-inheriting & b₃ is directed-sups-inheriting & b₁,b₃ are_isomorphic ) implies b₁ is algebraic ) )

proof end;

theorem Th35: :: WAYBEL13:35

for b₁ being lower-bounded LATTICE holds
( ( b₁ is algebraic implies ex b₂ being non empty set ex b₃ being closure Function of (BoolePoset b₂),(BoolePoset b₂) st
( b₃ is directed-sups-preserving & b₁, Image b₃ are_isomorphic ) ) & ( ex b₂ being set ex b₃ being closure Function of (BoolePoset b₂),(BoolePoset b₂) st
( b₃ is directed-sups-preserving & b₁, Image b₃ are_isomorphic ) implies b₁ is algebraic ) )

proof end;