:: WAYBEL_4 semantic presentation

definition

let c₁ be non empty reflexive RelStr ;
canceled;
func c₁ -waybelow -> Relation of a₁ means :Def2: :: WAYBEL_4:def 2
for b₁, b₂ being Element of a₁ holds
( [b₁,b₂] in a₂ iff b₁ << b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 WAYBEL_4:def 1 :

:: deftheorem Def2 defines -waybelow WAYBEL_4:def 2 :

definition

let c₁ be RelStr ;
func IntRel c₁ -> Relation of a₁ equals :: WAYBEL_4:def 3
the InternalRel of a₁;
coherence ;
correctness ;

end;

:: deftheorem Def3 defines IntRel WAYBEL_4:def 3 :

Lemma2: for b₁ being RelStr
for b₂, b₃ being Element of b₁ holds
( [b₂,b₃] in IntRel b₁ iff b₂ <= b₃ )
by ORDERS_2:def 9;

definition

let c₁ be RelStr ;
let c₂ be Relation of c₁;
attr a₂ is auxiliary(i) means :Def4: :: WAYBEL_4:def 4
for b₁, b₂ being Element of a₁ st [b₁,b₂] in a₂ holds
b₁ <= b₂;
attr a₂ is auxiliary(ii) means :Def5: :: WAYBEL_4:def 5
for b₁, b₂, b₃, b₄ being Element of a₁ st b₄ <= b₁ & [b₁,b₂] in a₂ & b₂ <= b₃ holds
[b₄,b₃] in a₂;

end;

:: deftheorem Def4 defines auxiliary(i) WAYBEL_4:def 4 :

:: deftheorem Def5 defines auxiliary(ii) WAYBEL_4:def 5 :

definition

let c₁ be non empty RelStr ;
let c₂ be Relation of c₁;
attr a₂ is auxiliary(iii) means :Def6: :: WAYBEL_4:def 6
for b₁, b₂, b₃ being Element of a₁ st [b₁,b₃] in a₂ & [b₂,b₃] in a₂ holds
[(b₁ "\/" b₂),b₃] in a₂;
attr a₂ is auxiliary(iv) means :Def7: :: WAYBEL_4:def 7
for b₁ being Element of a₁ holds [(Bottom a₁),b₁] in a₂;

end;

:: deftheorem Def6 defines auxiliary(iii) WAYBEL_4:def 6 :

:: deftheorem Def7 defines auxiliary(iv) WAYBEL_4:def 7 :

definition

let c₁ be non empty RelStr ;
let c₂ be Relation of c₁;
attr a₂ is auxiliary means :Def8: :: WAYBEL_4:def 8
( a₂ is auxiliary(i) & a₂ is auxiliary(ii) & a₂ is auxiliary(iii) & a₂ is auxiliary(iv) );

end;

:: deftheorem Def8 defines auxiliary WAYBEL_4:def 8 :

registration

let c₁ be non empty RelStr ;
cluster auxiliary -> auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of the carrier of a₁,the carrier of a₁;
coherence by Def8;
cluster auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) -> auxiliary Relation of the carrier of a₁,the carrier of a₁;
coherence by Def8;

end;

registration

let c₁ be transitive antisymmetric lower-bounded with_suprema RelStr ;
cluster auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Relation of the carrier of a₁,the carrier of a₁;
existence

proof end;

end;

theorem Th1: :: WAYBEL_4:1

for b₁ being lower-bounded sup-Semilattice
for b₂ being auxiliary(ii) auxiliary(iii) Relation of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st [b₃,b₅] in b₂ & [b₄,b₆] in b₂ holds
[(b₃ "\/" b₄),(b₅ "\/" b₆)] in b₂

proof end;

Lemma9: for b₁ being lower-bounded sup-Semilattice
for b₂ being auxiliary(i) auxiliary(ii) Relation of b₁ holds b₂ is transitive

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster auxiliary(i) auxiliary(ii) -> transitive Relation of the carrier of a₁,the carrier of a₁;
coherence by Lemma9;

end;

registration

let c₁ be RelStr ;
cluster IntRel a₁ -> auxiliary(i) ;
coherence

proof end;

end;

registration

let c₁ be transitive RelStr ;
cluster IntRel a₁ -> auxiliary(i) auxiliary(ii) ;
coherence

proof end;

end;

registration

let c₁ be antisymmetric with_suprema RelStr ;
cluster IntRel a₁ -> auxiliary(i) auxiliary(iii) ;
coherence

proof end;

end;

registration

let c₁ be non empty antisymmetric lower-bounded RelStr ;
cluster IntRel a₁ -> auxiliary(i) auxiliary(iv) ;
coherence

proof end;

end;

definition

let c₁ be lower-bounded sup-Semilattice;
func Aux c₁ -> set means :Def9: :: WAYBEL_4:def 9
for b₁ being set holds
( b₁ in a₂ iff b₁ is auxiliary Relation of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Aux WAYBEL_4:def 9 :

registration

let c₁ be lower-bounded sup-Semilattice;
cluster Aux a₁ -> non empty ;
coherence

proof end;

end;

Lemma11: for b₁ being lower-bounded sup-Semilattice
for b₂ being auxiliary(i) Relation of b₁
for b₃, b₄ being set st [b₃,b₄] in b₂ holds
[b₃,b₄] in IntRel b₁

proof end;

theorem Th2: :: WAYBEL_4:2

for b₁ being lower-bounded sup-Semilattice
for b₂ being auxiliary(i) Relation of b₁ holds b₂ c= IntRel b₁

proof end;

theorem Th3: :: WAYBEL_4:3

for b₁ being lower-bounded sup-Semilattice holds Top (InclPoset (Aux b₁)) = IntRel b₁

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster InclPoset (Aux a₁) -> upper-bounded ;
coherence

proof end;

end;

definition

let c₁ be non empty RelStr ;
func AuxBottom c₁ -> Relation of a₁ means :Def10: :: WAYBEL_4:def 10
for b₁, b₂ being Element of a₁ holds
( [b₁,b₂] in a₂ iff b₁ = Bottom a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines AuxBottom WAYBEL_4:def 10 :

registration

let c₁ be lower-bounded sup-Semilattice;
cluster AuxBottom a₁ -> transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ;
coherence

proof end;

end;

theorem Th4: :: WAYBEL_4:4

for b₁ being lower-bounded sup-Semilattice
for b₂ being auxiliary(iv) Relation of b₁ holds AuxBottom b₁ c= b₂

proof end;

theorem Th5: :: WAYBEL_4:5

for b₁ being lower-bounded sup-Semilattice holds Bottom (InclPoset (Aux b₁)) = AuxBottom b₁

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster InclPoset (Aux a₁) -> lower-bounded upper-bounded ;
coherence

proof end;

end;

theorem Th6: :: WAYBEL_4:6

for b₁ being lower-bounded sup-Semilattice
for b₂, b₃ being auxiliary(i) Relation of b₁ holds b₂ /\ b₃ is auxiliary(i) Relation of b₁

proof end;

theorem Th7: :: WAYBEL_4:7

for b₁ being lower-bounded sup-Semilattice
for b₂, b₃ being auxiliary(ii) Relation of b₁ holds b₂ /\ b₃ is auxiliary(ii) Relation of b₁

proof end;

theorem Th8: :: WAYBEL_4:8

for b₁ being lower-bounded sup-Semilattice
for b₂, b₃ being auxiliary(iii) Relation of b₁ holds b₂ /\ b₃ is auxiliary(iii) Relation of b₁

proof end;

theorem Th9: :: WAYBEL_4:9

for b₁ being lower-bounded sup-Semilattice
for b₂, b₃ being auxiliary(iv) Relation of b₁ holds b₂ /\ b₃ is auxiliary(iv) Relation of b₁

proof end;

theorem Th10: :: WAYBEL_4:10

for b₁ being lower-bounded sup-Semilattice
for b₂, b₃ being auxiliary Relation of b₁ holds b₂ /\ b₃ is auxiliary Relation of b₁

proof end;

theorem Th11: :: WAYBEL_4:11

for b₁ being lower-bounded sup-Semilattice
for b₂ being non empty Subset of (InclPoset (Aux b₁)) holds meet b₂ is auxiliary Relation of b₁

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster InclPoset (Aux a₁) -> lower-bounded upper-bounded with_infima ;
coherence

proof end;

end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster InclPoset (Aux a₁) -> lower-bounded upper-bounded with_infima complete ;
coherence

proof end;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
let c₃ be Relation of the carrier of c₁;
E21: { b₁ where B is Element of c₁ : [b₁,c₂] in c₃ } c= the carrier of c₁

proof end;

func c₃ -below c₂ -> Subset of a₁ equals :: WAYBEL_4:def 11
{ b₁ where B is Element of a₁ : [b₁,a₂] in a₃ } ;
correctness by E21;
E22: { b₁ where B is Element of c₁ : [c₂,b₁] in c₃ } c= the carrier of c₁

proof end;

func c₃ -above c₂ -> Subset of a₁ equals :: WAYBEL_4:def 12
{ b₁ where B is Element of a₁ : [a₂,b₁] in a₃ } ;
correctness by E22;

end;

:: deftheorem Def11 defines -below WAYBEL_4:def 11 :

:: deftheorem Def12 defines -above WAYBEL_4:def 12 :

theorem Th12: :: WAYBEL_4:12

for b₁ being lower-bounded sup-Semilattice
for b₂ being Element of b₁
for b₃ being auxiliary(i) Relation of b₁ holds b₃ -below b₂ c= downarrow b₂

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
let c₂ be Element of c₁;
let c₃ be auxiliary(iv) Relation of c₁;
cluster a₃ -below a₂ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be lower-bounded sup-Semilattice;
let c₂ be Element of c₁;
let c₃ be auxiliary(ii) Relation of c₁;
cluster a₃ -below a₂ -> lower ;
coherence

proof end;

end;

registration

let c₁ be lower-bounded sup-Semilattice;
let c₂ be Element of c₁;
let c₃ be auxiliary(iii) Relation of c₁;
cluster a₃ -below a₂ -> directed ;
coherence

proof end;

end;

definition

let c₁ be lower-bounded sup-Semilattice;
let c₂ be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of c₁;
func c₂ -below -> Function of a₁,(InclPoset (Ids a₁)) means :Def13: :: WAYBEL_4:def 13
for b₁ being Element of a₁ holds a₃ . b₁ = a₂ -below b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines -below WAYBEL_4:def 13 :

theorem Th13: :: WAYBEL_4:13

for b₁ being non empty RelStr
for b₂ being Relation of b₁
for b₃ being set
for b₄ being Element of b₁ holds
( b₃ in b₂ -below b₄ iff [b₃,b₄] in b₂ )

proof end;

theorem Th14: :: WAYBEL_4:14

for b₁ being set
for b₂ being sup-Semilattice
for b₃ being Relation of b₂
for b₄ being Element of b₂ holds
( b₁ in b₃ -above b₄ iff [b₄,b₁] in b₃ )

proof end;

Lemma24: for b₁ being lower-bounded with_suprema Poset
for b₂ being Relation of b₁
for b₃ being set
for b₄ being Element of b₁ holds
( b₃ in downarrow b₄ iff [b₃,b₄] in the InternalRel of b₁ )

proof end;

theorem Th15: :: WAYBEL_4:15

for b₁ being lower-bounded sup-Semilattice
for b₂ being auxiliary(i) Relation of b₁
for b₃ being Element of b₁ st b₂ = the InternalRel of b₁ holds
b₂ -below b₃ = downarrow b₃

proof end;

definition

let c₁ be non empty Poset;
func MonSet c₁ -> strict RelStr means :Def14: :: WAYBEL_4:def 14
for b₁ being set holds
( ( b₁ in the carrier of a₂ implies ex b₂ being Function of a₁,(InclPoset (Ids a₁)) st
( b₁ = b₂ & b₂ is monotone & ( for b₃ being Element of a₁ holds b₂ . b₃ c= downarrow b₃ ) ) ) & ( ex b₂ being Function of a₁,(InclPoset (Ids a₁)) st
( b₁ = b₂ & b₂ is monotone & ( for b₃ being Element of a₁ holds b₂ . b₃ c= downarrow b₃ ) ) implies b₁ in the carrier of a₂ ) & ( for b₂, b₃ being set holds
( [b₂,b₃] in the InternalRel of a₂ iff ex b₄, b₅ being Function of a₁,(InclPoset (Ids a₁)) st
( b₂ = b₄ & b₃ = b₅ & b₂ in the carrier of a₂ & b₃ in the carrier of a₂ & b₄ <= b₅ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines MonSet WAYBEL_4:def 14 :

theorem Th16: :: WAYBEL_4:16

for b₁ being lower-bounded sup-Semilattice holds MonSet b₁ is full SubRelStr of (InclPoset (Ids b₁)) |^ the carrier of b₁

proof end;

theorem Th17: :: WAYBEL_4:17

for b₁ being lower-bounded sup-Semilattice
for b₂ being auxiliary(ii) Relation of b₁
for b₃, b₄ being Element of b₁ st b₃ <= b₄ holds
b₂ -below b₃ c= b₂ -below b₄

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
let c₂ be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of c₁;
cluster a₂ -below -> monotone ;
coherence

proof end;

end;

theorem Th18: :: WAYBEL_4:18

for b₁ being lower-bounded sup-Semilattice
for b₂ being auxiliary Relation of b₁ holds b₂ -below in the carrier of (MonSet b₁)

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster MonSet a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th19: :: WAYBEL_4:19

for b₁ being lower-bounded sup-Semilattice holds IdsMap b₁ in the carrier of (MonSet b₁)

proof end;

theorem Th20: :: WAYBEL_4:20

for b₁ being lower-bounded sup-Semilattice
for b₂ being auxiliary Relation of b₁ holds b₂ -below <= IdsMap b₁

proof end;

theorem Th21: :: WAYBEL_4:21

for b₁ being non empty lower-bounded Poset
for b₂ being Ideal of b₁ holds Bottom b₁ in b₂

proof end;

theorem Th22: :: WAYBEL_4:22

for b₁ being non empty upper-bounded Poset
for b₂ being Filter of b₁ holds Top b₁ in b₂

proof end;

theorem Th23: :: WAYBEL_4:23

for b₁ being non empty lower-bounded Poset holds downarrow (Bottom b₁) = {(Bottom b₁)}

proof end;

theorem Th24: :: WAYBEL_4:24

for b₁ being non empty upper-bounded Poset holds uparrow (Top b₁) = {(Top b₁)}

proof end;

Lemma31: for b₁ being lower-bounded sup-Semilattice
for b₂ being Ideal of b₁ holds {(Bottom b₁)} c= b₂

proof end;

theorem Th25: :: WAYBEL_4:25

for b₁ being lower-bounded sup-Semilattice holds the carrier of b₁ --> {(Bottom b₁)} is Function of b₁,(InclPoset (Ids b₁))

proof end;

Lemma33: for b₁ being lower-bounded sup-Semilattice
for b₂ being Function of b₁,(InclPoset (Ids b₁)) st b₂ = the carrier of b₁ --> {(Bottom b₁)} holds
b₂ is monotone

proof end;

theorem Th26: :: WAYBEL_4:26

for b₁ being lower-bounded sup-Semilattice holds the carrier of b₁ --> {(Bottom b₁)} in the carrier of (MonSet b₁)

proof end;

theorem Th27: :: WAYBEL_4:27

for b₁ being lower-bounded sup-Semilattice
for b₂ being auxiliary Relation of b₁ holds [(the carrier of b₁ --> {(Bottom b₁)}),(b₂ -below )] in the InternalRel of (MonSet b₁)

proof end;

Lemma35: for b₁ being lower-bounded sup-Semilattice ex b₂ being Element of (MonSet b₁) st b₂ is_>=_than the carrier of (MonSet b₁)

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster MonSet a₁ -> non empty strict upper-bounded ;
coherence

proof end;

end;

definition

let c₁ be lower-bounded sup-Semilattice;
func Rel2Map c₁ -> Function of (InclPoset (Aux a₁)),(MonSet a₁) means :Def15: :: WAYBEL_4:def 15
for b₁ being auxiliary Relation of a₁ holds a₂ . b₁ = b₁ -below ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Rel2Map WAYBEL_4:def 15 :

theorem Th28: :: WAYBEL_4:28

for b₁ being lower-bounded sup-Semilattice
for b₂, b₃ being auxiliary Relation of b₁ st b₂ c= b₃ holds
b₂ -below <= b₃ -below

proof end;

theorem Th29: :: WAYBEL_4:29

for b₁ being lower-bounded sup-Semilattice
for b₂ being Element of b₁
for b₃, b₄ being Relation of b₁ st b₃ c= b₄ holds
b₃ -below b₂ c= b₄ -below b₂

proof end;

Lemma38: for b₁ being lower-bounded sup-Semilattice holds Rel2Map b₁ is monotone

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster Rel2Map a₁ -> monotone ;
coherence by Lemma38;

end;

definition

let c₁ be lower-bounded sup-Semilattice;
func Map2Rel c₁ -> Function of (MonSet a₁),(InclPoset (Aux a₁)) means :Def16: :: WAYBEL_4:def 16
for b₁ being set st b₁ in the carrier of (MonSet a₁) holds
ex b₂ being auxiliary Relation of a₁ st
( b₂ = a₂ . b₁ & ( for b₃, b₄ being set holds
( [b₃,b₄] in b₂ iff ex b₅, b₆ being Element of a₁ex b₇ being Function of a₁,(InclPoset (Ids a₁)) st
( b₅ = b₃ & b₆ = b₄ & b₇ = b₁ & b₅ in b₇ . b₆ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines Map2Rel WAYBEL_4:def 16 :

Lemma40: for b₁ being lower-bounded sup-Semilattice holds Map2Rel b₁ is monotone

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster Map2Rel a₁ -> monotone ;
coherence by Lemma40;

end;

theorem Th30: :: WAYBEL_4:30

for b₁ being lower-bounded sup-Semilattice holds (Map2Rel b₁) * (Rel2Map b₁) = id (dom (Rel2Map b₁))

proof end;

theorem Th31: :: WAYBEL_4:31

for b₁ being lower-bounded sup-Semilattice holds (Rel2Map b₁) * (Map2Rel b₁) = id the carrier of (MonSet b₁)

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster Rel2Map a₁ -> V5 monotone ;
coherence

proof end;

end;

theorem Th32: :: WAYBEL_4:32

for b₁ being lower-bounded sup-Semilattice holds (Rel2Map b₁) " = Map2Rel b₁

proof end;

theorem Th33: :: WAYBEL_4:33

for b₁ being lower-bounded sup-Semilattice holds Rel2Map b₁ is isomorphic

proof end;

theorem Th34: :: WAYBEL_4:34

for b₁ being complete LATTICE
for b₂ being Element of b₁ holds meet { b₃ where B is Ideal of b₁ : b₂ <= sup b₃ } = waybelow b₂

proof end;

scheme :: WAYBEL_4:sch 1
s1{ F₁() -> non empty set , P₁[ set ], F₂( set ) -> set , F₃( set ) -> set } :

ex b₁ being Function st
( dom b₁ = F₁() & ( for b₂ being Element of F₁() holds
( ( P₁[b₂] implies b₁ . b₂ = F₂(b₂) ) & ( P₁[b₂] implies b₁ . b₂ = F₃(b₂) ) ) ) )

proof end;

definition

let c₁ be Semilattice;
let c₂ be Ideal of c₁;
func DownMap c₂ -> Function of a₁,(InclPoset (Ids a₁)) means :Def17: :: WAYBEL_4:def 17
for b₁ being Element of a₁ holds
( ( b₁ <= sup a₂ implies a₃ . b₁ = (downarrow b₁) /\ a₂ ) & ( not b₁ <= sup a₂ implies a₃ . b₁ = downarrow b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines DownMap WAYBEL_4:def 17 :

Lemma46: for b₁ being Semilattice
for b₂ being Ideal of b₁ holds DownMap b₂ is monotone

proof end;

Lemma47: for b₁ being Semilattice
for b₂ being Element of b₁
for b₃ being Ideal of b₁ holds (DownMap b₃) . b₂ c= downarrow b₂

proof end;

theorem Th35: :: WAYBEL_4:35

for b₁ being Semilattice
for b₂ being Ideal of b₁ holds DownMap b₂ in the carrier of (MonSet b₁)

proof end;

theorem Th36: :: WAYBEL_4:36

for b₁ being reflexive antisymmetric with_infima RelStr
for b₂ being Element of b₁
for b₃ being non empty lower Subset of b₁ holds {b₂} "/\" b₃ = (downarrow b₂) /\ b₃

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Relation of c₁;
attr a₂ is approximating means :Def18: :: WAYBEL_4:def 18
for b₁ being Element of a₁ holds b₁ = sup (a₂ -below b₁);

end;

:: deftheorem Def18 defines approximating WAYBEL_4:def 18 :

definition

let c₁ be non empty Poset;
let c₂ be Function of c₁,(InclPoset (Ids c₁));
attr a₂ is approximating means :Def19: :: WAYBEL_4:def 19
for b₁ being Element of a₁ ex b₂ being Subset of a₁ st
( b₂ = a₂ . b₁ & b₁ = sup b₂ );

end;

:: deftheorem Def19 defines approximating WAYBEL_4:def 19 :

theorem Th37: :: WAYBEL_4:37

for b₁ being lower-bounded meet-continuous Semilattice
for b₂ being Ideal of b₁ holds DownMap b₂ is approximating

proof end;

Lemma53: for b₁ being complete LATTICE
for b₂ being Element of b₁
for b₃ being directed Subset of b₁ holds sup ({b₂} "/\" b₃) <= b₂

proof end;

theorem Th38: :: WAYBEL_4:38

for b₁ being lower-bounded continuous LATTICE holds b₁ is meet-continuous

proof end;

registration

cluster lower-bounded continuous -> lower-bounded meet-continuous RelStr ;
coherence by Th38;

end;

theorem Th39: :: WAYBEL_4:39

for b₁ being lower-bounded continuous LATTICE
for b₂ being Ideal of b₁ holds DownMap b₂ is approximating by Th37;

registration

let c₁ be non empty reflexive antisymmetric RelStr ;
cluster a₁ -waybelow -> auxiliary(i) ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive transitive RelStr ;
cluster a₁ -waybelow -> auxiliary(ii) ;
coherence

proof end;

end;

registration

let c₁ be with_suprema Poset;
cluster a₁ -waybelow -> auxiliary(i) auxiliary(ii) auxiliary(iii) ;
coherence

proof end;

end;

registration

let c₁ be non empty /\-complete Poset;
cluster a₁ -waybelow -> auxiliary(i) auxiliary(ii) auxiliary(iii) ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster a₁ -waybelow -> auxiliary(i) auxiliary(iv) ;
coherence

proof end;

end;

theorem Th40: :: WAYBEL_4:40

for b₁ being complete LATTICE
for b₂ being Element of b₁ holds (b₁ -waybelow ) -below b₂ = waybelow b₂

proof end;

theorem Th41: :: WAYBEL_4:41

for b₁ being LATTICE holds IntRel b₁ is approximating

proof end;

Lemma57: for b₁ being lower-bounded continuous LATTICE holds b₁ -waybelow is approximating

proof end;

registration

let c₁ be lower-bounded continuous LATTICE;
cluster a₁ -waybelow -> transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating ;
coherence by Lemma57;

end;

registration

let c₁ be complete LATTICE;
cluster transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating Relation of the carrier of a₁,the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be complete LATTICE;
defpred S₁[ set ] means a₁ is auxiliary approximating Relation of c₁;
func App c₁ -> set means :Def20: :: WAYBEL_4:def 20
for b₁ being set holds
( b₁ in a₂ iff b₁ is auxiliary approximating Relation of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines App WAYBEL_4:def 20 :

registration

let c₁ be complete LATTICE;
cluster App a₁ -> non empty ;
coherence

proof end;

end;

theorem Th42: :: WAYBEL_4:42

for b₁ being complete LATTICE
for b₂ being Function of b₁,(InclPoset (Ids b₁)) st b₂ is approximating & b₂ in the carrier of (MonSet b₁) holds
ex b₃ being auxiliary approximating Relation of b₁ st b₃ = (Map2Rel b₁) . b₂

proof end;

theorem Th43: :: WAYBEL_4:43

for b₁ being complete LATTICE
for b₂ being Element of b₁ holds meet { ((DownMap b₃) . b₂) where B is Ideal of b₁ : verum } = waybelow b₂

proof end;

theorem Th44: :: WAYBEL_4:44

for b₁ being lower-bounded meet-continuous LATTICE
for b₂ being Element of b₁ holds meet { (b₃ -below b₂) where B is auxiliary Relation of b₁ : b₃ in App b₁ } = waybelow b₂

proof end;

theorem Th45: :: WAYBEL_4:45

for b₁ being complete LATTICE holds
( b₁ is continuous iff for b₂ being auxiliary approximating Relation of b₁ holds
( b₁ -waybelow c= b₂ & b₁ -waybelow is approximating ) )

proof end;

theorem Th46: :: WAYBEL_4:46

for b₁ being complete LATTICE holds
( b₁ is continuous iff ( b₁ is meet-continuous & ex b₂ being auxiliary approximating Relation of b₁ st
for b₃ being auxiliary approximating Relation of b₁ holds b₂ c= b₃ ) )

proof end;

definition

let c₁ be RelStr ;
let c₂ be Relation of c₁;
attr a₂ is satisfying_SI means :Def21: :: WAYBEL_4:def 21
for b₁, b₂ being Element of a₁ st [b₁,b₂] in a₂ & b₁ <> b₂ holds
ex b₃ being Element of a₁ st
( [b₁,b₃] in a₂ & [b₃,b₂] in a₂ & b₁ <> b₃ );

end;

:: deftheorem Def21 defines satisfying_SI WAYBEL_4:def 21 :

notation

let c₁ be RelStr ;
let c₂ be Relation of c₁;
synonym c₂ satisfies_SI for satisfying_SI c₂;

end;

definition

let c₁ be RelStr ;
let c₂ be Relation of c₁;
attr a₂ is satisfying_INT means :Def22: :: WAYBEL_4:def 22
for b₁, b₂ being Element of a₁ st [b₁,b₂] in a₂ holds
ex b₃ being Element of a₁ st
( [b₁,b₃] in a₂ & [b₃,b₂] in a₂ );

end;

:: deftheorem Def22 defines satisfying_INT WAYBEL_4:def 22 :

notation

let c₁ be RelStr ;
let c₂ be Relation of c₁;
synonym c₂ satisfies_INT for satisfying_INT c₂;

end;

theorem Th47: :: WAYBEL_4:47

canceled;

theorem Th48: :: WAYBEL_4:48

for b₁ being RelStr
for b₂ being Relation of b₁ st b₂ satisfies_SI holds
b₂ satisfies_INT

proof end;

registration

let c₁ be non empty RelStr ;
cluster satisfying_SI -> satisfying_INT Relation of the carrier of a₁,the carrier of a₁;
coherence by Th48;

end;

theorem Th49: :: WAYBEL_4:49

for b₁ being complete LATTICE
for b₂, b₃ being Element of b₁
for b₄ being approximating Relation of b₁ st not b₂ <= b₃ holds
ex b₅ being Element of b₁ st
( [b₅,b₂] in b₄ & not b₅ <= b₃ )

proof end;

theorem Th50: :: WAYBEL_4:50

for b₁ being complete LATTICE
for b₂, b₃ being Element of b₁
for b₄ being auxiliary(i) auxiliary(iii) approximating Relation of b₁ st [b₂,b₃] in b₄ & b₂ <> b₃ holds
ex b₅ being Element of b₁ st
( b₂ <= b₅ & [b₅,b₃] in b₄ & b₂ <> b₅ )

proof end;

theorem Th51: :: WAYBEL_4:51

for b₁ being complete LATTICE
for b₂, b₃ being Element of b₁
for b₄ being auxiliary approximating Relation of b₁ st b₂ << b₃ & b₂ <> b₃ holds
ex b₅ being Element of b₁ st
( [b₂,b₅] in b₄ & [b₅,b₃] in b₄ & b₂ <> b₅ )

proof end;

theorem Th52: :: WAYBEL_4:52

for b₁ being lower-bounded continuous LATTICE holds b₁ -waybelow satisfies_SI

proof end;

registration

end;

theorem Th53: :: WAYBEL_4:53

for b₁ being lower-bounded continuous LATTICE
for b₂, b₃ being Element of b₁ st b₂ << b₃ holds
ex b₄ being Element of b₁ st
( b₂ << b₄ & b₄ << b₃ )

proof end;

theorem Th54: :: WAYBEL_4:54

for b₁ being lower-bounded continuous LATTICE
for b₂, b₃ being Element of b₁ holds
( b₂ << b₃ iff for b₄ being non empty directed Subset of b₁ st b₃ <= sup b₄ holds
ex b₅ being Element of b₁ st
( b₅ in b₄ & b₂ << b₅ ) )

proof end;

definition

let c₁ be RelStr ;
let c₂ be Subset of c₁;
let c₃ be Relation of the carrier of c₁;
pred c₂ is_directed_wrt c₃ means :Def23: :: WAYBEL_4:def 23
for b₁, b₂ being Element of a₁ st b₁ in a₂ & b₂ in a₂ holds
ex b₃ being Element of a₁ st
( b₃ in a₂ & [b₁,b₃] in a₃ & [b₂,b₃] in a₃ );

end;

:: deftheorem Def23 defines is_directed_wrt WAYBEL_4:def 23 :

theorem Th55: :: WAYBEL_4:55

for b₁ being RelStr
for b₂ being Subset of b₁ st b₂ is_directed_wrt the InternalRel of b₁ holds
b₂ is directed

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Relation;
pred c₂ is_maximal_wrt c₁,c₃ means :Def24: :: WAYBEL_4:def 24
( a₂ in a₁ & ( for b₁ being set holds
( not b₁ in a₁ or not b₁ <> a₂ or not [a₂,b₁] in a₃ ) ) );

end;

:: deftheorem Def24 defines is_maximal_wrt WAYBEL_4:def 24 :

definition

let c₁ be RelStr ;
let c₂ be set ;
let c₃ be Element of c₁;
pred c₃ is_maximal_in c₂ means :Def25: :: WAYBEL_4:def 25
a₃ is_maximal_wrt a₂,the InternalRel of a₁;

end;

:: deftheorem Def25 defines is_maximal_in WAYBEL_4:def 25 :

theorem Th56: :: WAYBEL_4:56

for b₁ being RelStr
for b₂ being set
for b₃ being Element of b₁ holds
( b₃ is_maximal_in b₂ iff ( b₃ in b₂ & ( for b₄ being Element of b₁ holds
( not b₄ in b₂ or not b₃ < b₄ ) ) ) )

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Relation;
pred c₂ is_minimal_wrt c₁,c₃ means :Def26: :: WAYBEL_4:def 26
( a₂ in a₁ & ( for b₁ being set holds
( not b₁ in a₁ or not b₁ <> a₂ or not [b₁,a₂] in a₃ ) ) );

end;

:: deftheorem Def26 defines is_minimal_wrt WAYBEL_4:def 26 :

definition

let c₁ be RelStr ;
let c₂ be set ;
let c₃ be Element of c₁;
pred c₃ is_minimal_in c₂ means :Def27: :: WAYBEL_4:def 27
a₃ is_minimal_wrt a₂,the InternalRel of a₁;

end;

:: deftheorem Def27 defines is_minimal_in WAYBEL_4:def 27 :

theorem Th57: :: WAYBEL_4:57

for b₁ being RelStr
for b₂ being set
for b₃ being Element of b₁ holds
( b₃ is_minimal_in b₂ iff ( b₃ in b₂ & ( for b₄ being Element of b₁ holds
( not b₄ in b₂ or not b₃ > b₄ ) ) ) )

proof end;

theorem Th58: :: WAYBEL_4:58

for b₁ being complete LATTICE
for b₂ being Relation of b₁ st b₂ satisfies_SI holds
for b₃ being Element of b₁ st ex b₄ being Element of b₁ st b₄ is_maximal_wrt b₂ -below b₃,b₂ holds
[b₃,b₃] in b₂

proof end;

theorem Th59: :: WAYBEL_4:59

for b₁ being complete LATTICE
for b₂ being Relation of b₁ st ( for b₃ being Element of b₁ st ex b₄ being Element of b₁ st b₄ is_maximal_wrt b₂ -below b₃,b₂ holds
[b₃,b₃] in b₂ ) holds
b₂ satisfies_SI

proof end;

theorem Th60: :: WAYBEL_4:60

for b₁ being complete LATTICE
for b₂ being auxiliary(ii) auxiliary(iii) Relation of b₁ st b₂ satisfies_INT holds
for b₃ being Element of b₁ holds b₂ -below b₃ is_directed_wrt b₂

proof end;

theorem Th61: :: WAYBEL_4:61

for b₁ being complete LATTICE
for b₂ being Relation of b₁ st ( for b₃ being Element of b₁ holds b₂ -below b₃ is_directed_wrt b₂ ) holds
b₂ satisfies_INT

proof end;

theorem Th62: :: WAYBEL_4:62

for b₁ being complete LATTICE
for b₂ being auxiliary(i) auxiliary(ii) auxiliary(iii) approximating Relation of b₁ st b₂ satisfies_INT holds
b₂ satisfies_SI

proof end;

registration

let c₁ be complete LATTICE;
cluster auxiliary approximating satisfying_INT -> transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT Relation of the carrier of a₁,the carrier of a₁;
coherence by Th62;

end;