:: WAYBEL_2 semantic presentation

registration

let c₁, c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
let c₄ be non empty Subset of c₁;
cluster a₃ .: a₄ -> non empty ;
coherence

proof end;

end;

registration

cluster non empty reflexive connected -> non empty with_suprema with_infima RelStr ;
coherence

proof end;

end;

registration

let c₁ be Chain;
cluster [#] a₁ -> directed ;
coherence ;

end;

theorem Th1: :: WAYBEL_2:1

for b₁ being up-complete Semilattice
for b₂ being non empty directed Subset of b₁
for b₃ being Element of b₁ holds ex_sup_of {b₃} "/\" b₂,b₁

proof end;

theorem Th2: :: WAYBEL_2:2

for b₁ being up-complete sup-Semilattice
for b₂ being non empty directed Subset of b₁
for b₃ being Element of b₁ holds ex_sup_of {b₃} "\/" b₂,b₁

proof end;

theorem Th3: :: WAYBEL_2:3

for b₁ being up-complete sup-Semilattice
for b₂, b₃ being non empty directed Subset of b₁ holds b₂ is_<=_than sup (b₂ "\/" b₃)

proof end;

theorem Th4: :: WAYBEL_2:4

for b₁ being up-complete sup-Semilattice
for b₂, b₃ being non empty directed Subset of b₁ holds sup (b₂ "\/" b₃) = (sup b₂) "\/" (sup b₃)

proof end;

theorem Th5: :: WAYBEL_2:5

for b₁ being up-complete Semilattice
for b₂ being non empty directed Subset of [:b₁,b₁:] holds { (sup ({b₃} "/\" (proj2 b₂))) where B is Element of b₁ : b₃ in proj1 b₂ } = { (sup b₃) where B is non empty directed Subset of b₁ : ex b₁ being Element of b₁ st
( b₃ = {b₄} "/\" (proj2 b₂) & b₄ in proj1 b₂ ) }

proof end;

theorem Th6: :: WAYBEL_2:6

for b₁ being Semilattice
for b₂ being non empty directed Subset of [:b₁,b₁:] holds union { b₃ where B is non empty directed Subset of b₁ : ex b₁ being Element of b₁ st
( b₃ = {b₄} "/\" (proj2 b₂) & b₄ in proj1 b₂ ) } = (proj1 b₂) "/\" (proj2 b₂)

proof end;

theorem Th7: :: WAYBEL_2:7

for b₁ being up-complete Semilattice
for b₂ being non empty directed Subset of [:b₁,b₁:] holds ex_sup_of union { b₃ where B is non empty directed Subset of b₁ : ex b₁ being Element of b₁ st
( b₃ = {b₄} "/\" (proj2 b₂) & b₄ in proj1 b₂ ) } ,b₁

proof end;

theorem Th8: :: WAYBEL_2:8

for b₁ being up-complete Semilattice
for b₂ being non empty directed Subset of [:b₁,b₁:] holds ex_sup_of { (sup b₃) where B is non empty directed Subset of b₁ : ex b₁ being Element of b₁ st
( b₃ = {b₄} "/\" (proj2 b₂) & b₄ in proj1 b₂ ) } ,b₁

proof end;

theorem Th9: :: WAYBEL_2:9

for b₁ being up-complete Semilattice
for b₂ being non empty directed Subset of [:b₁,b₁:] holds "\/" { (sup b₃) where B is non empty directed Subset of b₁ : ex b₁ being Element of b₁ st
( b₃ = {b₄} "/\" (proj2 b₂) & b₄ in proj1 b₂ ) } ,b₁ <= "\/" (union { b₃ where B is non empty directed Subset of b₁ : ex b₁ being Element of b₁ st
( b₃ = {b₄} "/\" (proj2 b₂) & b₄ in proj1 b₂ ) } ),b₁

proof end;

theorem Th10: :: WAYBEL_2:10

for b₁ being up-complete Semilattice
for b₂ being non empty directed Subset of [:b₁,b₁:] holds "\/" { (sup b₃) where B is non empty directed Subset of b₁ : ex b₁ being Element of b₁ st
( b₃ = {b₄} "/\" (proj2 b₂) & b₄ in proj1 b₂ ) } ,b₁ = "\/" (union { b₃ where B is non empty directed Subset of b₁ : ex b₁ being Element of b₁ st
( b₃ = {b₄} "/\" (proj2 b₂) & b₄ in proj1 b₂ ) } ),b₁

proof end;

registration

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

proof end;

end;

theorem Th11: :: WAYBEL_2:11

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

proof end;

theorem Th12: :: WAYBEL_2:12

for b₁ being non empty reflexive antisymmetric up-complete RelStr
for b₂ being non empty directed Subset of [:b₁,b₁:] holds sup b₂ = [(sup (proj1 b₂)),(sup (proj2 b₂))]

proof end;

theorem Th13: :: WAYBEL_2:13

for b₁, b₂ being RelStr
for b₃ being Subset of b₁
for b₄ being Function of b₁,b₂ st b₄ is monotone holds
b₄ .: (downarrow b₃) c= downarrow (b₄ .: b₃)

proof end;

theorem Th14: :: WAYBEL_2:14

for b₁, b₂ being RelStr
for b₃ being Subset of b₁
for b₄ being Function of b₁,b₂ st b₄ is monotone holds
b₄ .: (uparrow b₃) c= uparrow (b₄ .: b₃)

proof end;

registration

cluster non empty reflexive trivial -> non empty reflexive distributive complemented RelStr ;
coherence

proof end;

end;

registration

cluster non empty strict distributive complemented trivial RelStr ;
existence

proof end;

end;

theorem Th15: :: WAYBEL_2:15

for b₁ being complete distributive LATTICE
for b₂ being Element of b₁
for b₃ being finite Subset of b₁ holds sup ({b₂} "/\" b₃) = b₂ "/\" (sup b₃)

proof end;

theorem Th16: :: WAYBEL_2:16

for b₁ being complete distributive LATTICE
for b₂ being Element of b₁
for b₃ being finite Subset of b₁ holds inf ({b₂} "\/" b₃) = b₂ "\/" (inf b₃)

proof end;

theorem Th17: :: WAYBEL_2:17

for b₁ being complete distributive LATTICE
for b₂ being Element of b₁
for b₃ being finite Subset of b₁ holds b₂ "/\" preserves_sup_of b₃

proof end;

scheme :: WAYBEL_2:sch 1
s1{ F₁() -> non empty RelStr , F₂() -> prenet of F₁(), F₃( set ) -> Element of F₁() } :

ex b₁ being prenet of F₁() st
( RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of F₂(),the InternalRel of F₂() #) & ( for b₂ being Element of b₁ holds the mapping of b₁ . b₂ = F₃((the mapping of F₂() . b₂)) ) )

proof end;

theorem Th18: :: WAYBEL_2:18

for b₁ being non empty RelStr
for b₂ being prenet of b₁ st b₂ is eventually-directed holds
rng (netmap b₂,b₁) is directed

proof end;

theorem Th19: :: WAYBEL_2:19

for b₁ being non empty reflexive RelStr
for b₂ being non empty directed Subset of b₁
for b₃ being Function of b₂,the carrier of b₁ holds NetStr(# b₂,(the InternalRel of b₁ |_2 b₂),b₃ #) is prenet of b₁

proof end;

theorem Th20: :: WAYBEL_2:20

for b₁ being non empty reflexive RelStr
for b₂ being non empty directed Subset of b₁
for b₃ being Function of b₂,the carrier of b₁
for b₄ being prenet of b₁ st b₃ = id b₂ & b₄ = NetStr(# b₂,(the InternalRel of b₁ |_2 b₂),b₃ #) holds
b₄ is eventually-directed

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be NetStr of c₁;
func sup c₂ -> Element of a₁ equals :: WAYBEL_2:def 1
Sup ;
coherence ;

end;

:: deftheorem Def1 defines sup WAYBEL_2:def 1 :

definition

let c₁ be non empty RelStr ;
let c₂ be set ;
let c₃ be Function of c₂,the carrier of c₁;
func FinSups c₃ -> prenet of a₁ means :Def2: :: WAYBEL_2:def 2
ex b₁ being Function of Fin a₂,the carrier of a₁ st
for b₂ being Element of Fin a₂ holds
( b₁ . b₂ = sup (a₃ .: b₂) & a₄ = NetStr(# (Fin a₂),(RelIncl (Fin a₂)),b₁ #) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines FinSups WAYBEL_2:def 2 :

theorem Th21: :: WAYBEL_2:21

for b₁ being non empty RelStr
for b₂, b₃ being set
for b₄ being Function of b₂,the carrier of b₁ holds
( b₃ is Element of (FinSups b₄) iff b₃ is Element of Fin b₂ )

proof end;

registration

let c₁ be non empty reflexive antisymmetric complete RelStr ;
let c₂ be set ;
let c₃ be Function of c₂,the carrier of c₁;
cluster FinSups a₃ -> monotone ;
coherence

proof end;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
let c₃ be non empty NetStr of c₁;
func c₂ "/\" c₃ -> strict NetStr of a₁ means :Def3: :: WAYBEL_2:def 3
( RelStr(# the carrier of a₄,the InternalRel of a₄ #) = RelStr(# the carrier of a₃,the InternalRel of a₃ #) & ( for b₁ being Element of a₄ ex b₂ being Element of a₁ st
( b₂ = the mapping of a₃ . b₁ & the mapping of a₄ . b₁ = a₂ "/\" b₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines "/\" WAYBEL_2:def 3 :

theorem Th22: :: WAYBEL_2:22

for b₁ being non empty RelStr
for b₂ being non empty NetStr of b₁
for b₃ being Element of b₁
for b₄ being set holds
( b₄ is Element of b₂ iff b₄ is Element of (b₃ "/\" b₂) )

proof end;

registration

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
let c₃ be non empty NetStr of c₁;
cluster a₂ "/\" a₃ -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
let c₃ be prenet of c₁;
cluster a₂ "/\" a₃ -> non empty strict directed ;
coherence

proof end;

end;

theorem Th23: :: WAYBEL_2:23

for b₁ being non empty RelStr
for b₂ being Element of b₁
for b₃ being non empty NetStr of b₁ holds rng the mapping of (b₂ "/\" b₃) = {b₂} "/\" (rng the mapping of b₃)

proof end;

theorem Th24: :: WAYBEL_2:24

for b₁ being non empty RelStr
for b₂ being set
for b₃ being Function of b₂,the carrier of b₁ st ( for b₄ being set holds ex_sup_of b₃ .: b₄,b₁ ) holds
rng (netmap (FinSups b₃),b₁) c= finsups (rng b₃)

proof end;

theorem Th25: :: WAYBEL_2:25

for b₁ being non empty reflexive antisymmetric RelStr
for b₂ being set
for b₃ being Function of b₂,the carrier of b₁ holds rng b₃ c= rng (netmap (FinSups b₃),b₁)

proof end;

theorem Th26: :: WAYBEL_2:26

for b₁ being non empty reflexive antisymmetric RelStr
for b₂ being set
for b₃ being Function of b₂,the carrier of b₁ st ex_sup_of rng b₃,b₁ & ex_sup_of rng (netmap (FinSups b₃),b₁),b₁ & ( for b₄ being Element of Fin b₂ holds ex_sup_of b₃ .: b₄,b₁ ) holds
Sup = sup (FinSups b₃)

proof end;

theorem Th27: :: WAYBEL_2:27

for b₁ being transitive antisymmetric with_infima RelStr
for b₂ being prenet of b₁
for b₃ being Element of b₁ st b₂ is eventually-directed holds
b₃ "/\" b₂ is eventually-directed

proof end;

theorem Th28: :: WAYBEL_2:28

for b₁ being up-complete Semilattice st ( for b₂ being Element of b₁
for b₃ being non empty directed Subset of b₁ st b₂ <= sup b₃ holds
b₂ <= sup ({b₂} "/\" b₃) ) holds
for b₂ being non empty directed Subset of b₁
for b₃ being Element of b₁ holds b₃ "/\" (sup b₂) = sup ({b₃} "/\" b₂)

proof end;

theorem Th29: :: WAYBEL_2:29

for b₁ being with_suprema Poset st ( for b₂ being directed Subset of b₁
for b₃ being Element of b₁ holds b₃ "/\" (sup b₂) = sup ({b₃} "/\" b₂) ) holds
for b₂ being Subset of b₁
for b₃ being Element of b₁ st ex_sup_of b₂,b₁ holds
b₃ "/\" (sup b₂) = sup ({b₃} "/\" (finsups b₂))

proof end;

theorem Th30: :: WAYBEL_2:30

for b₁ being up-complete LATTICE st ( for b₂ being Subset of b₁
for b₃ being Element of b₁ holds b₃ "/\" (sup b₂) = sup ({b₃} "/\" (finsups b₂)) ) holds
for b₂ being non empty directed Subset of b₁
for b₃ being Element of b₁ holds b₃ "/\" (sup b₂) = sup ({b₃} "/\" b₂)

proof end;

definition

let c₁ be non empty RelStr ;
func inf_op c₁ -> Function of [:a₁,a₁:],a₁ means :Def4: :: WAYBEL_2:def 4
for b₁, b₂ being Element of a₁ holds a₂ . [b₁,b₂] = b₁ "/\" b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines inf_op WAYBEL_2:def 4 :

theorem Th31: :: WAYBEL_2:31

for b₁ being non empty RelStr
for b₂ being Element of [:b₁,b₁:] holds (inf_op b₁) . b₂ = (b₂ `1 ) "/\" (b₂ `2 )

proof end;

registration

let c₁ be transitive antisymmetric with_infima RelStr ;
cluster inf_op a₁ -> monotone ;
coherence

proof end;

end;

theorem Th32: :: WAYBEL_2:32

for b₁ being non empty RelStr
for b₂, b₃ being Subset of b₁ holds (inf_op b₁) .: [:b₂,b₃:] = b₂ "/\" b₃

proof end;

theorem Th33: :: WAYBEL_2:33

for b₁ being up-complete Semilattice
for b₂ being non empty directed Subset of [:b₁,b₁:] holds sup ((inf_op b₁) .: b₂) = sup ((proj1 b₂) "/\" (proj2 b₂))

proof end;

definition

let c₁ be non empty RelStr ;
func sup_op c₁ -> Function of [:a₁,a₁:],a₁ means :Def5: :: WAYBEL_2:def 5
for b₁, b₂ being Element of a₁ holds a₂ . [b₁,b₂] = b₁ "\/" b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines sup_op WAYBEL_2:def 5 :

theorem Th34: :: WAYBEL_2:34

for b₁ being non empty RelStr
for b₂ being Element of [:b₁,b₁:] holds (sup_op b₁) . b₂ = (b₂ `1 ) "\/" (b₂ `2 )

proof end;

registration

let c₁ be transitive antisymmetric with_suprema RelStr ;
cluster sup_op a₁ -> monotone ;
coherence

proof end;

end;

theorem Th35: :: WAYBEL_2:35

for b₁ being non empty RelStr
for b₂, b₃ being Subset of b₁ holds (sup_op b₁) .: [:b₂,b₃:] = b₂ "\/" b₃

proof end;

theorem Th36: :: WAYBEL_2:36

for b₁ being non empty complete Poset
for b₂ being non empty filtered Subset of [:b₁,b₁:] holds inf ((sup_op b₁) .: b₂) = inf ((proj1 b₂) "\/" (proj2 b₂))

proof end;

definition

let c₁ be non empty reflexive RelStr ;
attr a₁ is satisfying_MC means :Def6: :: WAYBEL_2:def 6
for b₁ being Element of a₁
for b₂ being non empty directed Subset of a₁ holds b₁ "/\" (sup b₂) = sup ({b₁} "/\" b₂);

end;

:: deftheorem Def6 defines satisfying_MC WAYBEL_2:def 6 :

definition

let c₁ be non empty reflexive RelStr ;
attr a₁ is meet-continuous means :Def7: :: WAYBEL_2:def 7
( a₁ is up-complete & a₁ is satisfying_MC );

end;

:: deftheorem Def7 defines meet-continuous WAYBEL_2:def 7 :

registration

cluster non empty reflexive trivial -> non empty reflexive satisfying_MC RelStr ;
coherence

proof end;

end;

registration

cluster non empty reflexive meet-continuous -> non empty reflexive up-complete satisfying_MC RelStr ;
coherence by Def7;
cluster non empty reflexive up-complete satisfying_MC -> non empty reflexive meet-continuous RelStr ;
coherence by Def7;

end;

registration

cluster non empty strict distributive complemented trivial satisfying_MC meet-continuous RelStr ;
existence

proof end;

end;

theorem Th37: :: WAYBEL_2:37

for b₁ being non empty reflexive RelStr st ( for b₂ being Subset of b₁
for b₃ being Element of b₁ holds b₃ "/\" (sup b₂) = "\/" { (b₃ "/\" b₄) where B is Element of b₁ : b₄ in b₂ } ,b₁ ) holds
b₁ is satisfying_MC

proof end;

theorem Th38: :: WAYBEL_2:38

for b₁ being up-complete Semilattice st SupMap b₁ is meet-preserving holds
for b₂, b₃ being Ideal of b₁ holds (sup b₂) "/\" (sup b₃) = sup (b₂ "/\" b₃)

proof end;

registration

let c₁ be up-complete sup-Semilattice;
cluster SupMap a₁ -> join-preserving ;
coherence

proof end;

end;

theorem Th39: :: WAYBEL_2:39

for b₁ being up-complete Semilattice st ( for b₂, b₃ being Ideal of b₁ holds (sup b₂) "/\" (sup b₃) = sup (b₂ "/\" b₃) ) holds
SupMap b₁ is meet-preserving

proof end;

theorem Th40: :: WAYBEL_2:40

for b₁ being up-complete Semilattice st ( for b₂, b₃ being Ideal of b₁ holds (sup b₂) "/\" (sup b₃) = sup (b₂ "/\" b₃) ) holds
for b₂, b₃ being non empty directed Subset of b₁ holds (sup b₂) "/\" (sup b₃) = sup (b₂ "/\" b₃)

proof end;

theorem Th41: :: WAYBEL_2:41

for b₁ being non empty reflexive RelStr st b₁ is satisfying_MC holds
for b₂ being Element of b₁
for b₃ being non empty prenet of b₁ st b₃ is eventually-directed holds
b₂ "/\" (sup b₃) = sup ({b₂} "/\" (rng (netmap b₃,b₁)))

proof end;

theorem Th42: :: WAYBEL_2:42

for b₁ being non empty reflexive RelStr st ( for b₂ being Element of b₁
for b₃ being prenet of b₁ st b₃ is eventually-directed holds
b₂ "/\" (sup b₃) = sup ({b₂} "/\" (rng (netmap b₃,b₁))) ) holds
b₁ is satisfying_MC

proof end;

theorem Th43: :: WAYBEL_2:43

for b₁ being non empty reflexive antisymmetric up-complete RelStr st inf_op b₁ is directed-sups-preserving holds
for b₂, b₃ being non empty directed Subset of b₁ holds (sup b₂) "/\" (sup b₃) = sup (b₂ "/\" b₃)

proof end;

theorem Th44: :: WAYBEL_2:44

for b₁ being non empty reflexive antisymmetric RelStr st ( for b₂, b₃ being non empty directed Subset of b₁ holds (sup b₂) "/\" (sup b₃) = sup (b₂ "/\" b₃) ) holds
b₁ is satisfying_MC

proof end;

theorem Th45: :: WAYBEL_2:45

for b₁ being non empty reflexive antisymmetric with_infima satisfying_MC RelStr
for b₂ being Element of b₁
for b₃ being non empty directed Subset of b₁ st b₂ <= sup b₃ holds
b₂ = sup ({b₂} "/\" b₃)

proof end;

theorem Th46: :: WAYBEL_2:46

for b₁ being up-complete Semilattice st ( for b₂ being Element of b₁
for b₃ being non empty directed Subset of b₁ st b₂ <= sup b₃ holds
b₂ <= sup ({b₂} "/\" b₃) ) holds
inf_op b₁ is directed-sups-preserving

proof end;

theorem Th47: :: WAYBEL_2:47

for b₁ being non empty reflexive antisymmetric complete RelStr st ( for b₂ being Element of b₁
for b₃ being prenet of b₁ st b₃ is eventually-directed holds
b₂ "/\" (sup b₃) = sup ({b₂} "/\" (rng (netmap b₃,b₁))) ) holds
for b₂ being Element of b₁
for b₃ being set
for b₄ being Function of b₃,the carrier of b₁ holds b₂ "/\" (Sup ) = sup (b₂ "/\" (FinSups b₄))

proof end;

theorem Th48: :: WAYBEL_2:48

for b₁ being complete Semilattice st ( for b₂ being Element of b₁
for b₃ being set
for b₄ being Function of b₃,the carrier of b₁ holds b₂ "/\" (Sup ) = sup (b₂ "/\" (FinSups b₄)) ) holds
for b₂ being Element of b₁
for b₃ being prenet of b₁ st b₃ is eventually-directed holds
b₂ "/\" (sup b₃) = sup ({b₂} "/\" (rng (netmap b₃,b₁)))

proof end;

theorem Th49: :: WAYBEL_2:49

for b₁ being up-complete LATTICE holds
( b₁ is meet-continuous iff ( SupMap b₁ is meet-preserving & SupMap b₁ is join-preserving ) )

proof end;

registration

let c₁ be meet-continuous LATTICE;
cluster SupMap a₁ -> meet-preserving join-preserving ;
coherence by Th49;

end;

theorem Th50: :: WAYBEL_2:50

for b₁ being up-complete LATTICE holds
( b₁ is meet-continuous iff for b₂, b₃ being Ideal of b₁ holds (sup b₂) "/\" (sup b₃) = sup (b₂ "/\" b₃) )

proof end;

theorem Th51: :: WAYBEL_2:51

for b₁ being up-complete LATTICE holds
( b₁ is meet-continuous iff for b₂, b₃ being non empty directed Subset of b₁ holds (sup b₂) "/\" (sup b₃) = sup (b₂ "/\" b₃) )

proof end;

theorem Th52: :: WAYBEL_2:52

for b₁ being up-complete LATTICE holds
( b₁ is meet-continuous iff for b₂ being Element of b₁
for b₃ being non empty directed Subset of b₁ st b₂ <= sup b₃ holds
b₂ = sup ({b₂} "/\" b₃) )

proof end;

theorem Th53: :: WAYBEL_2:53

for b₁ being up-complete Semilattice holds
( b₁ is meet-continuous iff inf_op b₁ is directed-sups-preserving )

proof end;

registration

let c₁ be meet-continuous Semilattice;
cluster inf_op a₁ -> monotone directed-sups-preserving ;
coherence by Th53;

end;

theorem Th54: :: WAYBEL_2:54

for b₁ being up-complete Semilattice holds
( b₁ is meet-continuous iff for b₂ being Element of b₁
for b₃ being non empty prenet of b₁ st b₃ is eventually-directed holds
b₂ "/\" (sup b₃) = sup ({b₂} "/\" (rng (netmap b₃,b₁))) )

proof end;

theorem Th55: :: WAYBEL_2:55

for b₁ being complete Semilattice holds
( b₁ is meet-continuous iff for b₂ being Element of b₁
for b₃ being set
for b₄ being Function of b₃,the carrier of b₁ holds b₂ "/\" (Sup ) = sup (b₂ "/\" (FinSups b₄)) )

proof end;

Lemma53: for b₁ being meet-continuous Semilattice
for b₂ being Element of b₁ holds b₂ "/\" is directed-sups-preserving

proof end;

registration

let c₁ be meet-continuous Semilattice;
let c₂ be Element of c₁;
cluster a₂ "/\" -> directed-sups-preserving ;
coherence by Lemma53;

end;

theorem Th56: :: WAYBEL_2:56

for b₁ being non empty complete Poset holds
( b₁ is Heyting iff ( b₁ is meet-continuous & b₁ is distributive ) )

proof end;

registration

cluster non empty complete Heyting -> non empty up-complete distributive satisfying_MC meet-continuous RelStr ;
coherence by Th56;
cluster non empty complete distributive meet-continuous -> non empty Heyting RelStr ;
coherence by Th56;

end;