:: YELLOW10 semantic presentation

registration

let c₁, c₂ be non empty upper-bounded RelStr ;
cluster [:a₁,a₂:] -> upper-bounded ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty lower-bounded RelStr ;
cluster [:a₁,a₂:] -> lower-bounded ;
coherence

proof end;

end;

theorem Th1: :: YELLOW10:1

for b₁, b₂ being non empty RelStr st [:b₁,b₂:] is upper-bounded holds
( b₁ is upper-bounded & b₂ is upper-bounded )

proof end;

theorem Th2: :: YELLOW10:2

for b₁, b₂ being non empty RelStr st [:b₁,b₂:] is lower-bounded holds
( b₁ is lower-bounded & b₂ is lower-bounded )

proof end;

theorem Th3: :: YELLOW10:3

for b₁, b₂ being non empty antisymmetric upper-bounded RelStr holds Top [:b₁,b₂:] = [(Top b₁),(Top b₂)]

proof end;

theorem Th4: :: YELLOW10:4

for b₁, b₂ being non empty antisymmetric lower-bounded RelStr holds Bottom [:b₁,b₂:] = [(Bottom b₁),(Bottom b₂)]

proof end;

theorem Th5: :: YELLOW10:5

for b₁, b₂ being non empty antisymmetric lower-bounded RelStr
for b₃ being Subset of [:b₁,b₂:] st ( [:b₁,b₂:] is complete or ex_sup_of b₃,[:b₁,b₂:] ) holds
sup b₃ = [(sup (proj1 b₃)),(sup (proj2 b₃))]

proof end;

theorem Th6: :: YELLOW10:6

for b₁, b₂ being non empty antisymmetric upper-bounded RelStr
for b₃ being Subset of [:b₁,b₂:] st ( [:b₁,b₂:] is complete or ex_inf_of b₃,[:b₁,b₂:] ) holds
inf b₃ = [(inf (proj1 b₃)),(inf (proj2 b₃))]

proof end;

theorem Th7: :: YELLOW10:7

for b₁, b₂ being non empty RelStr
for b₃, b₄ being Element of [:b₁,b₂:] holds
( b₃ is_<=_than {b₄} iff ( b₃ `1 is_<=_than {(b₄ `1 )} & b₃ `2 is_<=_than {(b₄ `2 )} ) )

proof end;

theorem Th8: :: YELLOW10:8

for b₁, b₂ being non empty RelStr
for b₃, b₄, b₅ being Element of [:b₁,b₂:] holds
( b₃ is_<=_than {b₄,b₅} iff ( b₃ `1 is_<=_than {(b₄ `1 ),(b₅ `1 )} & b₃ `2 is_<=_than {(b₄ `2 ),(b₅ `2 )} ) )

proof end;

theorem Th9: :: YELLOW10:9

for b₁, b₂ being non empty RelStr
for b₃, b₄ being Element of [:b₁,b₂:] holds
( b₃ is_>=_than {b₄} iff ( b₃ `1 is_>=_than {(b₄ `1 )} & b₃ `2 is_>=_than {(b₄ `2 )} ) )

proof end;

theorem Th10: :: YELLOW10:10

for b₁, b₂ being non empty RelStr
for b₃, b₄, b₅ being Element of [:b₁,b₂:] holds
( b₃ is_>=_than {b₄,b₅} iff ( b₃ `1 is_>=_than {(b₄ `1 ),(b₅ `1 )} & b₃ `2 is_>=_than {(b₄ `2 ),(b₅ `2 )} ) )

proof end;

theorem Th11: :: YELLOW10:11

for b₁, b₂ being non empty antisymmetric RelStr
for b₃, b₄ being Element of [:b₁,b₂:] holds
( ex_inf_of {b₃,b₄},[:b₁,b₂:] iff ( ex_inf_of {(b₃ `1 ),(b₄ `1 )},b₁ & ex_inf_of {(b₃ `2 ),(b₄ `2 )},b₂ ) )

proof end;

theorem Th12: :: YELLOW10:12

for b₁, b₂ being non empty antisymmetric RelStr
for b₃, b₄ being Element of [:b₁,b₂:] holds
( ex_sup_of {b₃,b₄},[:b₁,b₂:] iff ( ex_sup_of {(b₃ `1 ),(b₄ `1 )},b₁ & ex_sup_of {(b₃ `2 ),(b₄ `2 )},b₂ ) )

proof end;

theorem Th13: :: YELLOW10:13

for b₁, b₂ being antisymmetric with_infima RelStr
for b₃, b₄ being Element of [:b₁,b₂:] holds
( (b₃ "/\" b₄) `1 = (b₃ `1 ) "/\" (b₄ `1 ) & (b₃ "/\" b₄) `2 = (b₃ `2 ) "/\" (b₄ `2 ) )

proof end;

theorem Th14: :: YELLOW10:14

for b₁, b₂ being antisymmetric with_suprema RelStr
for b₃, b₄ being Element of [:b₁,b₂:] holds
( (b₃ "\/" b₄) `1 = (b₃ `1 ) "\/" (b₄ `1 ) & (b₃ "\/" b₄) `2 = (b₃ `2 ) "\/" (b₄ `2 ) )

proof end;

theorem Th15: :: YELLOW10:15

for b₁, b₂ being antisymmetric with_infima RelStr
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ holds [(b₃ "/\" b₄),(b₅ "/\" b₆)] = [b₃,b₅] "/\" [b₄,b₆]

proof end;

theorem Th16: :: YELLOW10:16

for b₁, b₂ being antisymmetric with_suprema RelStr
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ holds [(b₃ "\/" b₄),(b₅ "\/" b₆)] = [b₃,b₅] "\/" [b₄,b₆]

proof end;

definition

let c₁ be antisymmetric with_suprema with_infima RelStr ;
let c₂, c₃ be Element of c₁;
redefine pred is_a_complement_of as c₃ is_a_complement_of c₂;
symmetry

proof end;

end;

theorem Th17: :: YELLOW10:17

for b₁, b₂ being antisymmetric with_suprema with_infima bounded RelStr
for b₃, b₄ being Element of [:b₁,b₂:] holds
( b₃ is_a_complement_of b₄ iff ( b₃ `1 is_a_complement_of b₄ `1 & b₃ `2 is_a_complement_of b₄ `2 ) )

proof end;

theorem Th18: :: YELLOW10:18

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st [b₃,b₅] << [b₄,b₆] holds
( b₃ << b₄ & b₅ << b₆ )

proof end;

theorem Th19: :: YELLOW10:19

for b₁, b₂ being non empty up-complete Poset
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ holds
( [b₃,b₅] << [b₄,b₆] iff ( b₃ << b₄ & b₅ << b₆ ) )

proof end;

theorem Th20: :: YELLOW10:20

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃, b₄ being Element of [:b₁,b₂:] st b₃ << b₄ holds
( b₃ `1 << b₄ `1 & b₃ `2 << b₄ `2 )

proof end;

theorem Th21: :: YELLOW10:21

for b₁, b₂ being non empty up-complete Poset
for b₃, b₄ being Element of [:b₁,b₂:] holds
( b₃ << b₄ iff ( b₃ `1 << b₄ `1 & b₃ `2 << b₄ `2 ) )

proof end;

theorem Th22: :: YELLOW10:22

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃ being Element of [:b₁,b₂:] st b₃ is compact holds
( b₃ `1 is compact & b₃ `2 is compact )

proof end;

theorem Th23: :: YELLOW10:23

for b₁, b₂ being non empty up-complete Poset
for b₃ being Element of [:b₁,b₂:] st b₃ `1 is compact & b₃ `2 is compact holds
b₃ is compact

proof end;

theorem Th24: :: YELLOW10:24

for b₁, b₂ being antisymmetric with_infima RelStr
for b₃, b₄ being Subset of [:b₁,b₂:] holds
( proj1 (b₃ "/\" b₄) = (proj1 b₃) "/\" (proj1 b₄) & proj2 (b₃ "/\" b₄) = (proj2 b₃) "/\" (proj2 b₄) )

proof end;

theorem Th25: :: YELLOW10:25

for b₁, b₂ being antisymmetric with_suprema RelStr
for b₃, b₄ being Subset of [:b₁,b₂:] holds
( proj1 (b₃ "\/" b₄) = (proj1 b₃) "\/" (proj1 b₄) & proj2 (b₃ "\/" b₄) = (proj2 b₃) "\/" (proj2 b₄) )

proof end;

theorem Th26: :: YELLOW10:26

for b₁, b₂ being RelStr
for b₃ being Subset of [:b₁,b₂:] holds downarrow b₃ c= [:(downarrow (proj1 b₃)),(downarrow (proj2 b₃)):]

proof end;

theorem Th27: :: YELLOW10:27

for b₁, b₂ being RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂ holds [:(downarrow b₃),(downarrow b₄):] = downarrow [:b₃,b₄:]

proof end;

theorem Th28: :: YELLOW10:28

for b₁, b₂ being RelStr
for b₃ being Subset of [:b₁,b₂:] holds
( proj1 (downarrow b₃) c= downarrow (proj1 b₃) & proj2 (downarrow b₃) c= downarrow (proj2 b₃) )

proof end;

theorem Th29: :: YELLOW10:29

for b₁ being RelStr
for b₂ being reflexive RelStr
for b₃ being Subset of [:b₁,b₂:] holds proj1 (downarrow b₃) = downarrow (proj1 b₃)

proof end;

theorem Th30: :: YELLOW10:30

for b₁ being reflexive RelStr
for b₂ being RelStr
for b₃ being Subset of [:b₁,b₂:] holds proj2 (downarrow b₃) = downarrow (proj2 b₃)

proof end;

theorem Th31: :: YELLOW10:31

for b₁, b₂ being RelStr
for b₃ being Subset of [:b₁,b₂:] holds uparrow b₃ c= [:(uparrow (proj1 b₃)),(uparrow (proj2 b₃)):]

proof end;

theorem Th32: :: YELLOW10:32

for b₁, b₂ being RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂ holds [:(uparrow b₃),(uparrow b₄):] = uparrow [:b₃,b₄:]

proof end;

theorem Th33: :: YELLOW10:33

for b₁, b₂ being RelStr
for b₃ being Subset of [:b₁,b₂:] holds
( proj1 (uparrow b₃) c= uparrow (proj1 b₃) & proj2 (uparrow b₃) c= uparrow (proj2 b₃) )

proof end;

theorem Th34: :: YELLOW10:34

for b₁ being RelStr
for b₂ being reflexive RelStr
for b₃ being Subset of [:b₁,b₂:] holds proj1 (uparrow b₃) = uparrow (proj1 b₃)

proof end;

theorem Th35: :: YELLOW10:35

for b₁ being reflexive RelStr
for b₂ being RelStr
for b₃ being Subset of [:b₁,b₂:] holds proj2 (uparrow b₃) = uparrow (proj2 b₃)

proof end;

theorem Th36: :: YELLOW10:36

for b₁, b₂ being non empty RelStr
for b₃ being Element of b₁
for b₄ being Element of b₂ holds [:(downarrow b₃),(downarrow b₄):] = downarrow [b₃,b₄]

proof end;

theorem Th37: :: YELLOW10:37

for b₁, b₂ being non empty RelStr
for b₃ being Element of [:b₁,b₂:] holds
( proj1 (downarrow b₃) c= downarrow (b₃ `1 ) & proj2 (downarrow b₃) c= downarrow (b₃ `2 ) )

proof end;

theorem Th38: :: YELLOW10:38

for b₁ being non empty RelStr
for b₂ being non empty reflexive RelStr
for b₃ being Element of [:b₁,b₂:] holds proj1 (downarrow b₃) = downarrow (b₃ `1 )

proof end;

theorem Th39: :: YELLOW10:39

for b₁ being non empty reflexive RelStr
for b₂ being non empty RelStr
for b₃ being Element of [:b₁,b₂:] holds proj2 (downarrow b₃) = downarrow (b₃ `2 )

proof end;

theorem Th40: :: YELLOW10:40

for b₁, b₂ being non empty RelStr
for b₃ being Element of b₁
for b₄ being Element of b₂ holds [:(uparrow b₃),(uparrow b₄):] = uparrow [b₃,b₄]

proof end;

theorem Th41: :: YELLOW10:41

for b₁, b₂ being non empty RelStr
for b₃ being Element of [:b₁,b₂:] holds
( proj1 (uparrow b₃) c= uparrow (b₃ `1 ) & proj2 (uparrow b₃) c= uparrow (b₃ `2 ) )

proof end;

theorem Th42: :: YELLOW10:42

for b₁ being non empty RelStr
for b₂ being non empty reflexive RelStr
for b₃ being Element of [:b₁,b₂:] holds proj1 (uparrow b₃) = uparrow (b₃ `1 )

proof end;

theorem Th43: :: YELLOW10:43

for b₁ being non empty reflexive RelStr
for b₂ being non empty RelStr
for b₃ being Element of [:b₁,b₂:] holds proj2 (uparrow b₃) = uparrow (b₃ `2 )

proof end;

theorem Th44: :: YELLOW10:44

for b₁, b₂ being non empty up-complete Poset
for b₃ being Element of b₁
for b₄ being Element of b₂ holds [:(waybelow b₃),(waybelow b₄):] = waybelow [b₃,b₄]

proof end;

theorem Th45: :: YELLOW10:45

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃ being Element of [:b₁,b₂:] holds
( proj1 (waybelow b₃) c= waybelow (b₃ `1 ) & proj2 (waybelow b₃) c= waybelow (b₃ `2 ) )

proof end;

theorem Th46: :: YELLOW10:46

for b₁ being non empty up-complete Poset
for b₂ being non empty lower-bounded up-complete Poset
for b₃ being Element of [:b₁,b₂:] holds proj1 (waybelow b₃) = waybelow (b₃ `1 )

proof end;

theorem Th47: :: YELLOW10:47

for b₁ being non empty lower-bounded up-complete Poset
for b₂ being non empty up-complete Poset
for b₃ being Element of [:b₁,b₂:] holds proj2 (waybelow b₃) = waybelow (b₃ `2 )

proof end;

theorem Th48: :: YELLOW10:48

for b₁, b₂ being non empty up-complete Poset
for b₃ being Element of b₁
for b₄ being Element of b₂ holds [:(wayabove b₃),(wayabove b₄):] = wayabove [b₃,b₄]

proof end;

theorem Th49: :: YELLOW10:49

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃ being Element of [:b₁,b₂:] holds
( proj1 (wayabove b₃) c= wayabove (b₃ `1 ) & proj2 (wayabove b₃) c= wayabove (b₃ `2 ) )

proof end;

theorem Th50: :: YELLOW10:50

for b₁, b₂ being non empty up-complete Poset
for b₃ being Element of b₁
for b₄ being Element of b₂ holds [:(compactbelow b₃),(compactbelow b₄):] = compactbelow [b₃,b₄]

proof end;

theorem Th51: :: YELLOW10:51

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃ being Element of [:b₁,b₂:] holds
( proj1 (compactbelow b₃) c= compactbelow (b₃ `1 ) & proj2 (compactbelow b₃) c= compactbelow (b₃ `2 ) )

proof end;

theorem Th52: :: YELLOW10:52

for b₁ being non empty up-complete Poset
for b₂ being non empty lower-bounded up-complete Poset
for b₃ being Element of [:b₁,b₂:] holds proj1 (compactbelow b₃) = compactbelow (b₃ `1 )

proof end;

theorem Th53: :: YELLOW10:53

for b₁ being non empty lower-bounded up-complete Poset
for b₂ being non empty up-complete Poset
for b₃ being Element of [:b₁,b₂:] holds proj2 (compactbelow b₃) = compactbelow (b₃ `2 )

proof end;

registration

let c₁ be non empty reflexive RelStr ;
cluster empty -> Open M2( bool the carrier of a₁);
coherence

proof end;

end;

theorem Th54: :: YELLOW10:54

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃ being Subset of [:b₁,b₂:] st b₃ is Open holds
( proj1 b₃ is Open & proj2 b₃ is Open )

proof end;

theorem Th55: :: YELLOW10:55

for b₁, b₂ being non empty up-complete Poset
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ is Open & b₄ is Open holds
[:b₃,b₄:] is Open

proof end;

theorem Th56: :: YELLOW10:56

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃ being Subset of [:b₁,b₂:] st b₃ is inaccessible_by_directed_joins holds
( proj1 b₃ is inaccessible_by_directed_joins & proj2 b₃ is inaccessible_by_directed_joins )

proof end;

theorem Th57: :: YELLOW10:57

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃ being upper Subset of b₁
for b₄ being upper Subset of b₂ st b₃ is inaccessible_by_directed_joins & b₄ is inaccessible_by_directed_joins holds
[:b₃,b₄:] is inaccessible_by_directed_joins

proof end;

theorem Th58: :: YELLOW10:58

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st [:b₃,b₄:] is closed_under_directed_sups holds
( ( b₄ <> {} implies b₃ is closed_under_directed_sups ) & ( b₃ <> {} implies b₄ is closed_under_directed_sups ) )

proof end;

theorem Th59: :: YELLOW10:59

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ is closed_under_directed_sups & b₄ is closed_under_directed_sups holds
[:b₃,b₄:] is closed_under_directed_sups

proof end;

theorem Th60: :: YELLOW10:60

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr
for b₃ being Subset of [:b₁,b₂:] st b₃ has_the_property_(S) holds
( proj1 b₃ has_the_property_(S) & proj2 b₃ has_the_property_(S) )

proof end;

theorem Th61: :: YELLOW10:61

for b₁, b₂ being non empty up-complete Poset
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ has_the_property_(S) & b₄ has_the_property_(S) holds
[:b₃,b₄:] has_the_property_(S)

proof end;

theorem Th62: :: YELLOW10:62

for b₁, b₂ being non empty reflexive RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is /\-complete holds
b₂ is /\-complete

proof end;

registration

let c₁ be non empty reflexive /\-complete RelStr ;
cluster RelStr(# the carrier of a₁,the InternalRel of a₁ #) -> /\-complete ;
coherence by Th62;

end;

registration

let c₁, c₂ be non empty reflexive /\-complete RelStr ;
cluster [:a₁,a₂:] -> lower-bounded /\-complete ;
coherence

proof end;

end;

theorem Th63: :: YELLOW10:63

for b₁, b₂ being non empty reflexive RelStr st [:b₁,b₂:] is /\-complete holds
( b₁ is /\-complete & b₂ is /\-complete )

proof end;

registration

let c₁, c₂ be non empty antisymmetric with_suprema with_infima bounded complemented RelStr ;
cluster [:a₁,a₂:] -> lower-bounded upper-bounded complemented ;
coherence

proof end;

end;

theorem Th64: :: YELLOW10:64

for b₁, b₂ being antisymmetric with_suprema with_infima bounded RelStr st [:b₁,b₂:] is complemented holds
( b₁ is complemented & b₂ is complemented )

proof end;

registration

let c₁, c₂ be non empty antisymmetric with_suprema with_infima distributive RelStr ;
cluster [:a₁,a₂:] -> distributive ;
coherence

proof end;

end;

theorem Th65: :: YELLOW10:65

for b₁ being antisymmetric with_suprema with_infima RelStr
for b₂ being reflexive antisymmetric with_suprema with_infima RelStr st [:b₁,b₂:] is distributive holds
b₁ is distributive

proof end;

theorem Th66: :: YELLOW10:66

for b₁ being reflexive antisymmetric with_suprema with_infima RelStr
for b₂ being antisymmetric with_suprema with_infima RelStr st [:b₁,b₂:] is distributive holds
b₂ is distributive

proof end;

registration

let c₁, c₂ be meet-continuous Semilattice;
cluster [:a₁,a₂:] -> satisfying_MC ;
coherence

proof end;

end;

theorem Th67: :: YELLOW10:67

for b₁, b₂ being Semilattice st [:b₁,b₂:] is meet-continuous holds
( b₁ is meet-continuous & b₂ is meet-continuous )

proof end;

registration

let c₁, c₂ be non empty up-complete /\-complete satisfying_axiom_of_approximation Poset;
cluster [:a₁,a₂:] -> lower-bounded /\-complete satisfying_axiom_of_approximation ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty /\-complete continuous Poset;
cluster [:a₁,a₂:] -> lower-bounded /\-complete satisfying_axiom_of_approximation continuous ;
coherence

proof end;

end;

theorem Th68: :: YELLOW10:68

for b₁, b₂ being non empty lower-bounded up-complete Poset st [:b₁,b₂:] is continuous holds
( b₁ is continuous & b₂ is continuous )

proof end;

registration

let c₁, c₂ be lower-bounded up-complete satisfying_axiom_K sup-Semilattice;
cluster [:a₁,a₂:] -> /\-complete satisfying_axiom_K ;
coherence

proof end;

end;

registration

let c₁, c₂ be complete lower-bounded algebraic sup-Semilattice;
cluster [:a₁,a₂:] -> /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ;
coherence

proof end;

end;

theorem Th69: :: YELLOW10:69

for b₁, b₂ being non empty lower-bounded Poset st [:b₁,b₂:] is algebraic holds
( b₁ is algebraic & b₂ is algebraic )

proof end;

registration

let c₁, c₂ be lower-bounded arithmetic LATTICE;
cluster [:a₁,a₂:] -> /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ;
coherence

proof end;

end;

theorem Th70: :: YELLOW10:70

for b₁, b₂ being lower-bounded LATTICE st [:b₁,b₂:] is arithmetic holds
( b₁ is arithmetic & b₂ is arithmetic )

proof end;