:: Meet-continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received October 10, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

registration
let X, Y be non empty set ;
let f be Function of X,Y;
let Z be non empty Subset of X;
clusterf .: Z ->  non empty ;
coherence
 not f .: Z is empty
proofend;
end;

registration
cluster non empty reflexive connected  ->  non empty with_suprema with_infima for RelStr ;
coherence
 for b1 being non empty RelStr st b1 is reflexive & b1 is connected holds
( b1 is with_infima & b1 is with_suprema )
proofend;
end;

registration
let C be Chain;
cluster [#] C ->  directed ;
coherence
 [#] C is directed ;
end;

theorem Th1: :: WAYBEL_2:1
for L being up-complete Semilattice
for D being non empty directed Subset of L
for x being Element of L holds ex_sup_of {x} "/\" D,L
proofend;

theorem :: WAYBEL_2:2
for L being up-complete sup-Semilattice
for D being non empty directed Subset of L
for x being Element of L holds ex_sup_of {x} "\/" D,L
proofend;

theorem Th3: :: WAYBEL_2:3
for L being up-complete sup-Semilattice
for A, B being non empty directed Subset of L holds A is_<=_than sup (A "\/" B)
proofend;

theorem Th4: :: WAYBEL_2:4
for L being up-complete sup-Semilattice
for A, B being non empty directed Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)
proofend;

theorem Th5: :: WAYBEL_2:5
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds  {  (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D  }  =  {  (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) &amp; x in proj1 D )  }
proofend;

theorem Th6: :: WAYBEL_2:6
for L being Semilattice
for D being non empty directed Subset of [:L,L:] holds union  {  X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) &amp; x in proj1 D )  }  = (proj1 D) "/\" (proj2 D)
proofend;

theorem Th7: :: WAYBEL_2:7
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds ex_sup_of union  {  X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) &amp; x in proj1 D )  }  ,L
proofend;

theorem Th8: :: WAYBEL_2:8
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds ex_sup_of  {  (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) &amp; x in proj1 D )  }  ,L
proofend;

theorem Th9: :: WAYBEL_2:9
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds "\/" ( {  (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) &amp; x in proj1 D )  }  ,L) <= "\/" ((union  {  X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) &amp; x in proj1 D )  }  ),L)
proofend;

theorem Th10: :: WAYBEL_2:10
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds "\/" ( {  (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) &amp; x in proj1 D )  }  ,L) = "\/" ((union  {  X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) &amp; x in proj1 D )  }  ),L)
proofend;

registration
let S, T be non empty reflexive up-complete RelStr ;
cluster[:S,T:] ->  up-complete ;
coherence
 [:S,T:] is up-complete
proofend;
end;

theorem :: WAYBEL_2:11
for S, T being non empty reflexive antisymmetric RelStr st [:S,T:] is up-complete holds
( S is up-complete &amp; T is up-complete )
proofend;

theorem Th12: :: WAYBEL_2:12
for L being non empty reflexive antisymmetric up-complete RelStr
for D being non empty directed Subset of [:L,L:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))]
proofend;

theorem Th13: :: WAYBEL_2:13
for S1, S2 being RelStr
for D being Subset of S1
for f being Function of S1,S2 st f is monotone holds
f .: (downarrow D) c= downarrow (f .: D)
proofend;

theorem Th14: :: WAYBEL_2:14
for S1, S2 being RelStr
for D being Subset of S1
for f being Function of S1,S2 st f is monotone holds
f .: (uparrow D) c= uparrow (f .: D)
proofend;

registration
cluster1 -element reflexive  -> 1 -element reflexive distributive complemented for RelStr ;
coherence
 for b1 being 1 -element reflexive RelStr holds
( b1 is distributive &amp; b1 is complemented )
proofend;
end;

registration
cluster non empty 1 -element strict V70() reflexive transitive antisymmetric non void with_suprema with_infima for RelStr ;
existence
 ex b1 being LATTICE st
( b1 is strict &amp; b1 is 1 -element )
proofend;
end;

theorem Th15: :: WAYBEL_2:15
for H being distributive complete LATTICE
for a being Element of H
for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X)
proofend;

theorem :: WAYBEL_2:16
for H being distributive complete LATTICE
for a being Element of H
for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X)
proofend;

theorem Th17: :: WAYBEL_2:17
for H being distributive complete LATTICE
for a being Element of H
for X being finite Subset of H holds a "/\" preserves_sup_of X
proofend;

begin

scheme :: WAYBEL_2:sch 1
ExNet{ F1() ->  non empty RelStr , F2() ->  prenet of F1(), F3( set ) ->  Element of F1() } :
 ex M being prenet of F1() st
( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) &amp; ( for i being Element of M holds the mapping of M . i = F3(( the mapping of F2() . i)) ) )
proofend;

theorem Th18: :: WAYBEL_2:18
for L being non empty RelStr
for N being prenet of L st N is eventually-directed holds
rng (netmap (N,L)) is directed
proofend;

theorem Th19: :: WAYBEL_2:19
for L being non empty reflexive RelStr
for D being non empty directed Subset of L
for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L
proofend;

theorem Th20: :: WAYBEL_2:20
for L being non empty reflexive RelStr
for D being non empty directed Subset of L
for n being Function of D, the carrier of L
for N being prenet of L st n = id D &amp; N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds
N is eventually-directed
proofend;

definition
let L be non empty RelStr ;
let N be NetStr over L;
func sup N ->  Element of L equals :: WAYBEL_2:def 1
 Sup ;
coherence
 Sup is Element of L ;
end;

:: deftheorem  defines sup WAYBEL_2:def_1_:_
 for L being non empty RelStr
for N being NetStr over L holds sup N = Sup ;

definition
let L be non empty RelStr ;
let J be set ;
let f be Function of J, the carrier of L;
func FinSups f ->  prenet of L means :Def2: :: WAYBEL_2:def 2
 ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) &amp; it = NetStr(# (Fin J),(RelIncl (Fin J)),g #) );
existence
 ex b1 being prenet of L ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) &amp; b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) )
proofend;
uniqueness
 for b1, b2 being prenet of L st ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) &amp; b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) &amp; ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) &amp; b2 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines FinSups WAYBEL_2:def_2_:_
 for L being non empty RelStr
for J being set
for f being Function of J, the carrier of L
for b4 being prenet of L holds
( b4 = FinSups f iff ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) &amp; b4 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) );

theorem :: WAYBEL_2:21
for L being non empty RelStr
for J, x being set
for f being Function of J, the carrier of L holds
( x is Element of (FinSups f) iff x is Element of Fin J )
proofend;

registration
let L be non empty reflexive antisymmetric complete RelStr ;
let J be set ;
let f be Function of J, the carrier of L;
cluster FinSups f ->  monotone ;
coherence
 FinSups f is monotone
proofend;
end;

definition
let L be non empty RelStr ;
let x be Element of L;
let N be non empty NetStr over L;
funcx "/\" N ->  strict NetStr over L means :Def3: :: WAYBEL_2:def 3
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; ( for i being Element of it ex y being Element of L st
( y = the mapping of N . i &amp; the mapping of it . i = x "/\" y ) ) );
existence
 ex b1 being strict NetStr over L st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; ( for i being Element of b1 ex y being Element of L st
( y = the mapping of N . i &amp; the mapping of b1 . i = x "/\" y ) ) )
proofend;
uniqueness
 for b1, b2 being strict NetStr over L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; ( for i being Element of b1 ex y being Element of L st
( y = the mapping of N . i &amp; the mapping of b1 . i = x "/\" y ) ) &amp; RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; ( for i being Element of b2 ex y being Element of L st
( y = the mapping of N . i &amp; the mapping of b2 . i = x "/\" y ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines "/\" WAYBEL_2:def_3_:_
 for L being non empty RelStr
for x being Element of L
for N being non empty NetStr over L
for b4 being strict NetStr over L holds
( b4 = x "/\" N iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; ( for i being Element of b4 ex y being Element of L st
( y = the mapping of N . i &amp; the mapping of b4 . i = x "/\" y ) ) ) );

theorem Th22: :: WAYBEL_2:22
for L being non empty RelStr
for N being non empty NetStr over L
for x being Element of L
for y being set holds
( y is Element of N iff y is Element of (x "/\" N) )
proofend;

registration
let L be non empty RelStr ;
let x be Element of L;
let N be non empty NetStr over L;
clusterx "/\" N ->  non empty strict ;
coherence
 not x "/\" N is empty
proofend;
end;

registration
let L be non empty RelStr ;
let x be Element of L;
let N be prenet of L;
clusterx "/\" N ->  strict directed ;
coherence
 x "/\" N is directed
proofend;
end;

theorem Th23: :: WAYBEL_2:23
for L being non empty RelStr
for x being Element of L
for F being non empty NetStr over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)
proofend;

theorem Th24: :: WAYBEL_2:24
for L being non empty RelStr
for J being set
for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds
rng (netmap ((FinSups f),L)) c= finsups (rng f)
proofend;

theorem Th25: :: WAYBEL_2:25
for L being non empty reflexive antisymmetric RelStr
for J being set
for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L))
proofend;

theorem Th26: :: WAYBEL_2:26
for L being non empty reflexive antisymmetric RelStr
for J being set
for f being Function of J, the carrier of L st ex_sup_of rng f,L &amp; ex_sup_of rng (netmap ((FinSups f),L)),L &amp; ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds
Sup = sup (FinSups f)
proofend;

theorem Th27: :: WAYBEL_2:27
for L being transitive antisymmetric with_infima RelStr
for N being prenet of L
for x being Element of L st N is eventually-directed holds
x "/\" N is eventually-directed
proofend;

theorem Th28: :: WAYBEL_2:28
for L being up-complete Semilattice st ( for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ) holds
for D being non empty directed Subset of L
for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D)
proofend;

theorem :: WAYBEL_2:29
for L being with_suprema Poset st ( for X being directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) holds
for X being Subset of L
for x being Element of L st ex_sup_of X,L holds
x "/\" (sup X) = sup ({x} "/\" (finsups X))
proofend;

theorem :: WAYBEL_2:30
for L being up-complete LATTICE st ( for X being Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ) holds
for X being non empty directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X)
proofend;

begin

definition
let L be non empty RelStr ;
func inf_op L ->  Function of [:L,L:],L means :Def4: :: WAYBEL_2:def 4
 for x, y being Element of L holds it . (x,y) = x "/\" y;
existence
 ex b1 being Function of [:L,L:],L st
for x, y being Element of L holds b1 . (x,y) = x "/\" y
proofend;
uniqueness
 for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . (x,y) = x "/\" y ) &amp; ( for x, y being Element of L holds b2 . (x,y) = x "/\" y ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines inf_op WAYBEL_2:def_4_:_
 for L being non empty RelStr
for b2 being Function of [:L,L:],L holds
( b2 = inf_op L iff for x, y being Element of L holds b2 . (x,y) = x "/\" y );

theorem Th31: :: WAYBEL_2:31
for L being non empty RelStr
for x being Element of [:L,L:] holds (inf_op L) . x = (x `1) "/\" (x `2)
proofend;

registration
let L be transitive antisymmetric with_infima RelStr ;
cluster inf_op L ->  monotone ;
coherence
 inf_op L is monotone
proofend;
end;

theorem Th32: :: WAYBEL_2:32
for S being non empty RelStr
for D1, D2 being Subset of S holds (inf_op S) .: [:D1,D2:] = D1 "/\" D2
proofend;

theorem Th33: :: WAYBEL_2:33
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D))
proofend;

definition
let L be non empty RelStr ;
func sup_op L ->  Function of [:L,L:],L means :Def5: :: WAYBEL_2:def 5
 for x, y being Element of L holds it . (x,y) = x "\/" y;
existence
 ex b1 being Function of [:L,L:],L st
for x, y being Element of L holds b1 . (x,y) = x "\/" y
proofend;
uniqueness
 for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . (x,y) = x "\/" y ) &amp; ( for x, y being Element of L holds b2 . (x,y) = x "\/" y ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines sup_op WAYBEL_2:def_5_:_
 for L being non empty RelStr
for b2 being Function of [:L,L:],L holds
( b2 = sup_op L iff for x, y being Element of L holds b2 . (x,y) = x "\/" y );

theorem Th34: :: WAYBEL_2:34
for L being non empty RelStr
for x being Element of [:L,L:] holds (sup_op L) . x = (x `1) "\/" (x `2)
proofend;

registration
let L be transitive antisymmetric with_suprema RelStr ;
cluster sup_op L ->  monotone ;
coherence
 sup_op L is monotone
proofend;
end;

theorem Th35: :: WAYBEL_2:35
for S being non empty RelStr
for D1, D2 being Subset of S holds (sup_op S) .: [:D1,D2:] = D1 "\/" D2
proofend;

theorem :: WAYBEL_2:36
for L being non empty complete Poset
for D being non empty filtered Subset of [:L,L:] holds inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D))
proofend;

begin

:: Def 4.1, s.30
definition
let R be non empty reflexive RelStr ;
attrR is satisfying_MC  means :Def6: :: WAYBEL_2:def 6
 for x being Element of R
for D being non empty directed Subset of R holds x "/\" (sup D) = sup ({x} "/\" D);
end;

:: deftheorem Def6 defines satisfying_MC WAYBEL_2:def_6_:_
 for R being non empty reflexive RelStr holds
( R is satisfying_MC iff for x being Element of R
for D being non empty directed Subset of R holds x "/\" (sup D) = sup ({x} "/\" D) );

definition
let R be non empty reflexive RelStr ;
attrR is meet-continuous  means :Def7: :: WAYBEL_2:def 7
( R is up-complete &amp; R is satisfying_MC );
end;

:: deftheorem Def7 defines meet-continuous WAYBEL_2:def_7_:_
 for R being non empty reflexive RelStr holds
( R is meet-continuous iff ( R is up-complete &amp; R is satisfying_MC ) );

registration
cluster1 -element reflexive  -> 1 -element reflexive satisfying_MC for RelStr ;
coherence
 for b1 being 1 -element reflexive RelStr holds b1 is satisfying_MC
proofend;
end;

registration
cluster non empty reflexive meet-continuous  ->  non empty reflexive up-complete satisfying_MC for RelStr ;
coherence
 for b1 being non empty reflexive RelStr st b1 is meet-continuous holds
( b1 is up-complete &amp; b1 is satisfying_MC ) by Def7;
cluster non empty reflexive up-complete satisfying_MC  ->  non empty reflexive meet-continuous for RelStr ;
coherence
 for b1 being non empty reflexive RelStr st b1 is up-complete &amp; b1 is satisfying_MC holds
b1 is meet-continuous by Def7;
end;

theorem Th37: :: WAYBEL_2:37
for S being non empty reflexive RelStr st ( for X being Subset of S
for x being Element of S holds x "/\" (sup X) = "\/" ( {  (x "/\" y) where y is Element of S : y in X  }  ,S) ) holds
S is satisfying_MC
proofend;

:: Th 4.2, s.30, 1 => 2
theorem Th38: :: WAYBEL_2:38
for L being up-complete Semilattice st SupMap L is meet-preserving holds
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
proofend;

registration
let L be up-complete sup-Semilattice;
cluster SupMap L ->  join-preserving ;
coherence
 SupMap L is join-preserving
proofend;
end;

:: Th 4.2, s.30, 2 => 1
theorem Th39: :: WAYBEL_2:39
for L being up-complete Semilattice st ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) holds
SupMap L is meet-preserving
proofend;

:: Th 4.2, s.30, 2 => 3
theorem Th40: :: WAYBEL_2:40
for L being up-complete Semilattice st ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) holds
for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
proofend;

:: Th 4.2, s.30, 4 => 7
theorem Th41: :: WAYBEL_2:41
for L being non empty reflexive RelStr st L is satisfying_MC holds
for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
proofend;

:: Th 4.2, s.30, 7 => 4
theorem Th42: :: WAYBEL_2:42
for L being non empty reflexive RelStr st ( for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds
L is satisfying_MC
proofend;

:: Th 4.2, s.30, 6 => 3
theorem Th43: :: WAYBEL_2:43
for L being non empty reflexive antisymmetric up-complete RelStr st inf_op L is directed-sups-preserving holds
for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
proofend;

:: Th 4.2, s.30, 3 => 4
theorem Th44: :: WAYBEL_2:44
for L being non empty reflexive antisymmetric RelStr st ( for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) holds
L is satisfying_MC
proofend;

:: Th 4.2, s.30, MC => 5
theorem Th45: :: WAYBEL_2:45
for L being non empty reflexive antisymmetric with_infima satisfying_MC RelStr
for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D)
proofend;

:: Th 4.2, s.30, 5 => 6
theorem Th46: :: WAYBEL_2:46
for L being up-complete Semilattice st ( for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ) holds
inf_op L is directed-sups-preserving
proofend;

:: Th 4.2, s.30, 7 => 8
theorem Th47: :: WAYBEL_2:47
for L being non empty reflexive antisymmetric complete RelStr st ( for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds
for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))
proofend;

:: Th 4.2, s.30, 8 => 7
theorem Th48: :: WAYBEL_2:48
for L being complete Semilattice st ( for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) holds
for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
proofend;

:: Th 4.2, s.30, 4 <=> 1
theorem Th49: :: WAYBEL_2:49
for L being up-complete LATTICE holds
( L is meet-continuous iff ( SupMap L is meet-preserving &amp; SupMap L is join-preserving ) )
proofend;

registration
let L be meet-continuous LATTICE;
cluster SupMap L ->  meet-preserving join-preserving ;
coherence
 ( SupMap L is meet-preserving &amp; SupMap L is join-preserving ) by Th49;
end;

:: Th 4.2, s.30, 4 <=> 2
theorem Th50: :: WAYBEL_2:50
for L being up-complete LATTICE holds
( L is meet-continuous iff for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) )
proofend;

:: Th 4.2, s.30, 4 <=> 3
theorem Th51: :: WAYBEL_2:51
for L being up-complete LATTICE holds
( L is meet-continuous iff for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) )
proofend;

:: Th 4.2, s.30, 4 <=> 5
theorem :: WAYBEL_2:52
for L being up-complete LATTICE holds
( L is meet-continuous iff for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D) )
proofend;

:: Th 4.2, s.30, 4 <=> 6
theorem Th53: :: WAYBEL_2:53
for L being up-complete Semilattice holds
( L is meet-continuous iff inf_op L is directed-sups-preserving )
proofend;

registration
let L be meet-continuous Semilattice;
cluster inf_op L ->  directed-sups-preserving ;
coherence
 inf_op L is directed-sups-preserving by Th53;
end;

:: Th 4.2, s.30, 4 <=> 7
theorem Th54: :: WAYBEL_2:54
for L being up-complete Semilattice holds
( L is meet-continuous iff for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )
proofend;

:: Th 4.2, s.30, 4 <=> 8
theorem :: WAYBEL_2:55
for L being complete Semilattice holds
( L is meet-continuous iff for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) )
proofend;

Lm1:  for L being meet-continuous Semilattice
for x being Element of L holds x "/\" is directed-sups-preserving
proofend;

registration
let L be meet-continuous Semilattice;
let x be Element of L;
clusterx "/\"  ->  directed-sups-preserving ;
coherence
 x "/\" is directed-sups-preserving by Lm1;
end;

:: Remark 4.3 s.31
theorem Th56: :: WAYBEL_2:56
for H being non empty complete Poset holds
( H is Heyting iff ( H is meet-continuous &amp; H is distributive ) )
proofend;

registration
cluster non empty reflexive transitive antisymmetric Heyting complete  ->  non empty distributive meet-continuous for RelStr ;
coherence
 for b1 being non empty Poset st b1 is complete &amp; b1 is Heyting holds
( b1 is meet-continuous &amp; b1 is distributive ) by Th56;
cluster non empty reflexive transitive antisymmetric distributive complete meet-continuous  ->  non empty Heyting for RelStr ;
coherence
 for b1 being non empty Poset st b1 is complete &amp; b1 is meet-continuous &amp; b1 is distributive holds
b1 is Heyting by Th56;
end;