:: WAYBEL_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

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

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

theorem Th1: :: WAYBEL_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: WAYBEL_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th3: :: WAYBEL_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being up-complete sup-Semilattice
for A, B being non empty directed Subset of L holds A is_<=_than sup (A "\/" B)
proof end;

theorem Th4: :: WAYBEL_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th5: :: WAYBEL_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) & x in proj1 D )
}
proof end;

theorem Th6: :: WAYBEL_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) & x in proj1 D )
}
= (proj1 D) "/\" (proj2 D)
proof end;

theorem Th7: :: WAYBEL_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) & x in proj1 D )
}
,L
proof end;

theorem Th8: :: WAYBEL_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) & x in proj1 D )
}
,L
proof end;

theorem Th9: :: WAYBEL_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) & 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) & x in proj1 D )
}
)
,L
proof end;

theorem Th10: :: WAYBEL_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) & 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) & x in proj1 D )
}
)
,L
proof end;

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

theorem :: WAYBEL_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty reflexive antisymmetric RelStr st [:S,T:] is up-complete holds
( S is up-complete & T is up-complete )
proof end;

theorem Th12: :: WAYBEL_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))]
proof end;

theorem Th13: :: WAYBEL_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th14: :: WAYBEL_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

registration
cluster non empty reflexive trivial -> non empty reflexive distributive complemented RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is trivial holds
( b1 is distributive & b1 is complemented )
proof end;
end;

registration
cluster non empty strict distributive complemented trivial RelStr ;
existence
ex b1 being LATTICE st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

theorem Th15: :: WAYBEL_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being complete distributive LATTICE
for a being Element of H
for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X)
proof end;

theorem :: WAYBEL_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being complete distributive LATTICE
for a being Element of H
for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X)
proof end;

theorem Th17: :: WAYBEL_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being complete distributive LATTICE
for a being Element of H
for X being finite Subset of H holds a "/\" preserves_sup_of X
proof end;

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() #) & ( for i being Element of M holds the mapping of M . i = F3((the mapping of F2() . i)) ) )
proof end;

theorem Th18: :: WAYBEL_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for N being prenet of L st N is eventually-directed holds
rng (netmap N,L) is directed
proof end;

theorem Th19: :: WAYBEL_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th20: :: WAYBEL_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & N = NetStr(# D,(the InternalRel of L |_2 D),n #) holds
N is eventually-directed
proof end;

definition
let L be non empty RelStr ;
let N be NetStr of 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 of 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) & 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) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) )
proof end;
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) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & 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) & b2 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) holds
b1 = b2
proof end;
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) & b4 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) );

theorem :: WAYBEL_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

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
proof end;
end;

definition
let L be non empty RelStr ;
let x be Element of L;
let N be non empty NetStr of L;
func x "/\" N -> strict NetStr of 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 #) & ( for i being Element of it ex y being Element of L st
( y = the mapping of N . i & the mapping of it . i = x "/\" y ) ) );
existence
ex b1 being strict NetStr of L st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of N,the InternalRel of N #) & ( for i being Element of b1 ex y being Element of L st
( y = the mapping of N . i & the mapping of b1 . i = x "/\" y ) ) )
proof end;
uniqueness
for b1, b2 being strict NetStr of L st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of N,the InternalRel of N #) & ( for i being Element of b1 ex y being Element of L st
( y = the mapping of N . i & the mapping of b1 . i = x "/\" y ) ) & RelStr(# the carrier of b2,the InternalRel of b2 #) = RelStr(# the carrier of N,the InternalRel of N #) & ( for i being Element of b2 ex y being Element of L st
( y = the mapping of N . i & the mapping of b2 . i = x "/\" y ) ) holds
b1 = b2
proof end;
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 of L
for b4 being strict NetStr of L holds
( b4 = x "/\" N iff ( RelStr(# the carrier of b4,the InternalRel of b4 #) = RelStr(# the carrier of N,the InternalRel of N #) & ( for i being Element of b4 ex y being Element of L st
( y = the mapping of N . i & the mapping of b4 . i = x "/\" y ) ) ) );

theorem Th22: :: WAYBEL_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for N being non empty NetStr of L
for x being Element of L
for y being set holds
( y is Element of N iff y is Element of (x "/\" N) )
proof end;

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

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

theorem Th23: :: WAYBEL_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for x being Element of L
for F being non empty NetStr of L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)
proof end;

theorem Th24: :: WAYBEL_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th25: :: WAYBEL_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th26: :: WAYBEL_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ex_sup_of rng (netmap (FinSups f),L),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds
Sup = sup (FinSups f)
proof end;

theorem Th27: :: WAYBEL_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th28: :: WAYBEL_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: WAYBEL_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

theorem :: WAYBEL_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

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
proof end;
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . [x,y] = x "/\" y ) & ( for x, y being Element of L holds b2 . [x,y] = x "/\" y ) holds
b1 = b2
proof end;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for x being Element of [:L,L:] holds (inf_op L) . x = (x `1 ) "/\" (x `2 )
proof end;

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

theorem Th32: :: WAYBEL_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty RelStr
for D1, D2 being Subset of S holds (inf_op S) .: [:D1,D2:] = D1 "/\" D2
proof end;

theorem Th33: :: WAYBEL_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

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
proof end;
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . [x,y] = x "\/" y ) & ( for x, y being Element of L holds b2 . [x,y] = x "\/" y ) holds
b1 = b2
proof end;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for x being Element of [:L,L:] holds (sup_op L) . x = (x `1 ) "\/" (x `2 )
proof end;

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

theorem Th35: :: WAYBEL_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty RelStr
for D1, D2 being Subset of S holds (sup_op S) .: [:D1,D2:] = D1 "\/" D2
proof end;

theorem :: WAYBEL_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

definition
let R be non empty reflexive RelStr ;
attr R 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 ;
attr R is meet-continuous means :Def7: :: WAYBEL_2:def 7
( R is up-complete & 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 & R is satisfying_MC ) );

registration
cluster non empty reflexive trivial -> non empty reflexive satisfying_MC RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is trivial holds
b1 is satisfying_MC
proof end;
end;

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

registration
cluster non empty strict distributive complemented trivial satisfying_MC meet-continuous RelStr ;
existence
ex b1 being LATTICE st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

theorem Th37: :: WAYBEL_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th38: :: WAYBEL_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

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

theorem Th39: :: WAYBEL_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th40: :: WAYBEL_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th41: :: WAYBEL_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive RelStr st L is satisfying_MC holds
for x being Element of L
for N being non empty prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap N,L)))
proof end;

theorem Th42: :: WAYBEL_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th43: :: WAYBEL_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th44: :: WAYBEL_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th45: :: WAYBEL_2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th46: :: WAYBEL_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th47: :: WAYBEL_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

theorem Th48: :: WAYBEL_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)))
proof end;

theorem Th49: :: WAYBEL_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being up-complete LATTICE holds
( L is meet-continuous iff ( SupMap L is meet-preserving & SupMap L is join-preserving ) )
proof end;

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

theorem Th50: :: WAYBEL_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th51: :: WAYBEL_2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: WAYBEL_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th53: :: WAYBEL_2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being up-complete Semilattice holds
( L is meet-continuous iff inf_op L is directed-sups-preserving )
proof end;

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

theorem Th54: :: WAYBEL_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being up-complete Semilattice holds
( L is meet-continuous iff for x being Element of L
for N being non empty prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap N,L))) )
proof end;

theorem :: WAYBEL_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) )
proof end;

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

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

theorem Th56: :: WAYBEL_2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being non empty complete Poset holds
( H is Heyting iff ( H is meet-continuous & H is distributive ) )
proof end;

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