:: Algebraic and Arithmetic Lattices :: by Robert Milewski :: :: Received March 4, 1997 :: Copyright (c) 1997-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, RELAT_2, ORDERS_2, SUBSET_1, XXREAL_0, WAYBEL_8, TARSKI, RCOMP_1, STRUCT_0, YELLOW_0, LATTICE3, CARD_FIL, LATTICES, WAYBEL_0, WAYBEL_5, GROUP_6, WAYBEL10, YELLOW_1, FINSET_1, SETFAM_1, REWRITE1, RELAT_1, FUNCT_1, ZFMISC_1, CAT_1, EQREL_1, WELLORD2, ORDINAL2, WAYBEL_3, SEQM_3, PBOOLE, CARD_3, WELLORD1, WAYBEL_1, YELLOW_2; notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1, RELAT_1, ORDERS_1, ORDERS_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, PBOOLE, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL10; constructors DOMAIN_1, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL10, RELSET_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL10; requirements SUBSET, BOOLE; definitions TARSKI; equalities YELLOW_2, STRUCT_0; expansions TARSKI; theorems TARSKI, ZFMISC_1, SETFAM_1, ORDERS_2, FUNCT_1, FUNCT_2, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, CARD_3, WAYBEL_1, WAYBEL_3, WAYBEL_4, WAYBEL_5, WAYBEL_8, WAYBEL10, XBOOLE_0, XBOOLE_1; schemes FUNCT_2, PARTFUN1; begin :: Preliminaries theorem Th1: for L be non empty reflexive transitive RelStr for x,y be Element of L holds x <= y implies compactbelow x c= compactbelow y proof let L be non empty reflexive transitive RelStr; let x,y be Element of L; assume A1: x <= y; now let z be object; assume z in compactbelow x; then z in {v where v is Element of L: x >= v & v is compact} by WAYBEL_8:def 2; then consider z9 be Element of L such that A2: z9 = z and A3: x >= z9 and A4: z9 is compact; z9 <= y by A1,A3,ORDERS_2:3; hence z in compactbelow y by A2,A4,WAYBEL_8:4; end; hence thesis; end; theorem Th2: for L be non empty reflexive RelStr for x be Element of L holds compactbelow x is Subset of CompactSublatt L proof let L be non empty reflexive RelStr; let x be Element of L; now let v be object; assume v in compactbelow x; then v in {z where z is Element of L: x >= z & z is compact} by WAYBEL_8:def 2; then ex v1 be Element of L st v1 = v & x >= v1 & v1 is compact; hence v in the carrier of CompactSublatt L by WAYBEL_8:def 1; end; hence thesis by TARSKI:def 3; end; theorem Th3: for L be RelStr for S be SubRelStr of L for X be Subset of S holds X is Subset of L proof let L be RelStr; let S be SubRelStr of L; let X be Subset of S; the carrier of S c= the carrier of L by YELLOW_0:def 13; hence thesis by XBOOLE_1:1; end; theorem Th4: for L be with_suprema non empty reflexive transitive RelStr holds the carrier of L is Ideal of L proof let L be with_suprema non empty reflexive transitive RelStr; [#]L is Ideal of L; hence thesis; end; theorem Th5: for L1 be lower-bounded non empty reflexive antisymmetric RelStr for L2 be non empty reflexive antisymmetric RelStr st the RelStr of L1 = the RelStr of L2 & L1 is up-complete holds the carrier of CompactSublatt L1 = the carrier of CompactSublatt L2 proof let L1 be lower-bounded non empty reflexive antisymmetric RelStr; let L2 be non empty reflexive antisymmetric RelStr; assume that A1: the RelStr of L1 = the RelStr of L2 and A2: L1 is up-complete; now reconsider L29 = L2 as lower-bounded non empty reflexive antisymmetric RelStr by A1,YELLOW_0:13; let x be object; assume A3: x in the carrier of CompactSublatt L2; then x is Element of CompactSublatt L29; then reconsider x2 = x as Element of L2 by YELLOW_0:58; reconsider x1 = x2 as Element of L1 by A1; A4: x2 is compact by A3,WAYBEL_8:def 1; L2 is up-complete by A1,A2,WAYBEL_8:15; then x1 is compact by A1,A4,WAYBEL_8:9; hence x in the carrier of CompactSublatt L1 by WAYBEL_8:def 1; end; then A5: the carrier of CompactSublatt L2 c= the carrier of CompactSublatt L1; now let x be object; assume A6: x in the carrier of CompactSublatt L1; then reconsider x1 = x as Element of L1 by YELLOW_0:58; reconsider x2 = x1 as Element of L2 by A1; x1 is compact by A6,WAYBEL_8:def 1; then x2 is compact by A1,A2,WAYBEL_8:9; hence x in the carrier of CompactSublatt L2 by WAYBEL_8:def 1; end; then the carrier of CompactSublatt L1 c= the carrier of CompactSublatt L2; hence thesis by A5,XBOOLE_0:def 10; end; begin :: Algebraic and Arithmetic Lattices theorem Th6: :: COROLLARY 4.10. for L be algebraic lower-bounded LATTICE for S be CLSubFrame of L holds S is algebraic proof let L be algebraic lower-bounded LATTICE; let S be CLSubFrame of L; the RelStr of S = Image closure_op S by WAYBEL10:18; then (the RelStr of S) is algebraic by WAYBEL_8:24; hence thesis by WAYBEL_8:17; end; theorem Th7: :: EXAMPLES 4.11.(2) for X,E be set for L be CLSubFrame of BoolePoset X holds E in the carrier of CompactSublatt L iff ex F be Element of BoolePoset X st F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E proof let X,E be set; let L be CLSubFrame of BoolePoset X; A1: the carrier of L c= the carrier of BoolePoset X by YELLOW_0:def 13; A2: L is complete LATTICE by YELLOW_2:30; thus E in the carrier of CompactSublatt L implies ex F be Element of BoolePoset X st F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E proof A3: (closure_op L).:([#]CompactSublatt (BoolePoset X)) = [#]CompactSublatt Image (closure_op L) by WAYBEL_8:25 .= [#]CompactSublatt (the RelStr of L) by WAYBEL10:18 .= the carrier of CompactSublatt (the RelStr of L); assume E in the carrier of CompactSublatt L; then E in (closure_op L).:([#]CompactSublatt (BoolePoset X)) by A2,A3,Th5; then consider x be object such that A4: x in dom (closure_op L) and A5: x in [#]CompactSublatt (BoolePoset X) and A6: E = (closure_op L).x by FUNCT_1:def 6; reconsider F = x as Element of BoolePoset X by A4; id(BoolePoset X) <= closure_op L by WAYBEL_1:def 14; then id(BoolePoset X).F <= (closure_op L).F by YELLOW_2:9; then F <= (closure_op L).F; then A7: F c= (closure_op L).F by YELLOW_1:2; (closure_op L).x in rng (closure_op L) by A4,FUNCT_1:def 3; then (closure_op L).x in the carrier of Image (closure_op L) by YELLOW_0:def 15; then (closure_op L).x in the carrier of the RelStr of L by WAYBEL10:18; then A8: (closure_op L).x in { Y where Y is Element of L : F c= Y } by A7; take F; F is compact by A5,WAYBEL_8:def 1; hence F is finite by WAYBEL_8:28; A9: (uparrow F) /\ the carrier of L c= { Y where Y is Element of L : F c= Y } proof let z be object; assume A10: z in (uparrow F) /\ the carrier of L; then reconsider z9 = z as Element of BoolePoset X; z in uparrow F by A10,XBOOLE_0:def 4; then F <= z9 by WAYBEL_0:18; then A11: F c= z9 by YELLOW_1:2; z in the carrier of L by A10,XBOOLE_0:def 4; hence thesis by A11; end; { Y where Y is Element of L : F c= Y } c= (uparrow F) /\ the carrier of L proof let z be object; assume z in { Y where Y is Element of L : F c= Y }; then consider z9 be Element of L such that A12: z = z9 and A13: F c= z9; reconsider z1 = z9 as Element of BoolePoset X by A1; F <= z1 by A13,YELLOW_1:2; then z in uparrow F by A12,WAYBEL_0:18; hence thesis by A12,XBOOLE_0:def 4; end; then A14: (uparrow F) /\ the carrier of L = { Y where Y is Element of L : F c= Y } by A9,XBOOLE_0:def 10; thus A15: E = "/\"((uparrow F) /\ the carrier of L,BoolePoset X) by A6, WAYBEL10:def 5 .= meet { Y where Y is Element of L : F c= Y } by A8,A14,YELLOW_1:20; now let v be object; assume A16: v in F; now let V be set; assume V in { Y where Y is Element of L : F c= Y }; then ex V9 be Element of L st V = V9 & F c= V9; hence v in V by A16; end; hence v in E by A8,A15,SETFAM_1:def 1; end; hence thesis; end; thus ( ex F be Element of BoolePoset X st F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) implies E in the carrier of CompactSublatt L proof given F be Element of BoolePoset X such that A17: F is finite and A18: E = meet { Y where Y is Element of L : F c= Y } and F c= E; F is compact by A17,WAYBEL_8:28; then A19: F in [#]CompactSublatt (BoolePoset X) by WAYBEL_8:def 1; A20: (uparrow F) /\ the carrier of L c= { Y where Y is Element of L : F c= Y } proof let z be object; assume A21: z in (uparrow F) /\ the carrier of L; then reconsider z9 = z as Element of BoolePoset X; z in uparrow F by A21,XBOOLE_0:def 4; then F <= z9 by WAYBEL_0:18; then A22: F c= z9 by YELLOW_1:2; z in the carrier of L by A21,XBOOLE_0:def 4; hence thesis by A22; end; { Y where Y is Element of L : F c= Y } c= (uparrow F) /\ the carrier of L proof let z be object; assume z in { Y where Y is Element of L : F c= Y }; then consider z9 be Element of L such that A23: z = z9 and A24: F c= z9; reconsider z1 = z9 as Element of BoolePoset X by A1; F <= z1 by A24,YELLOW_1:2; then z in uparrow F by A23,WAYBEL_0:18; hence thesis by A23,XBOOLE_0:def 4; end; then A25: (uparrow F) /\ the carrier of L = { Y where Y is Element of L : F c= Y } by A20,XBOOLE_0:def 10; id(BoolePoset X) <= closure_op L by WAYBEL_1:def 14; then id(BoolePoset X).F <= (closure_op L).F by YELLOW_2:9; then F <= (closure_op L).F; then A26: F c= (closure_op L).F by YELLOW_1:2; F in the carrier of BoolePoset X; then A27: F in dom (closure_op L) by FUNCT_2:def 1; then (closure_op L).F in rng (closure_op L) by FUNCT_1:def 3; then (closure_op L).F in the carrier of Image (closure_op L) by YELLOW_0:def 15; then (closure_op L).F in the carrier of the RelStr of L by WAYBEL10:18; then (closure_op L).F in { Y where Y is Element of L : F c= Y } by A26; then E = "/\"((uparrow F) /\ the carrier of L,BoolePoset X) by A18,A25, YELLOW_1:20 .= (closure_op L).F by WAYBEL10:def 5; then A28: E in (closure_op L).:([#]CompactSublatt (BoolePoset X)) by A27,A19, FUNCT_1:def 6; (closure_op L).:([#]CompactSublatt (BoolePoset X)) = [#] CompactSublatt Image (closure_op L) by WAYBEL_8:25 .= [#]CompactSublatt (the RelStr of L) by WAYBEL10:18 .= the carrier of CompactSublatt (the RelStr of L); hence thesis by A2,A28,Th5; end; end; theorem Th8: for L be lower-bounded sup-Semilattice holds InclPoset Ids L is CLSubFrame of BoolePoset the carrier of L proof let L be lower-bounded sup-Semilattice; now let x be object; assume x in Ids L; then x in the set of all X where X is Ideal of L by WAYBEL_0:def 23; then ex x9 be Ideal of L st x9 = x; hence x in bool the carrier of L; end; then Ids L is Subset-Family of L by TARSKI:def 3; then reconsider InIdL = InclPoset Ids L as non empty full SubRelStr of BoolePoset the carrier of L by YELLOW_1:5; A1: for X be directed Subset of InIdL st X <> {} & ex_sup_of X,BoolePoset the carrier of L holds "\/"(X,BoolePoset the carrier of L) in the carrier of InIdL proof let X be directed Subset of InIdL; assume that A2: X <> {} and ex_sup_of X,BoolePoset the carrier of L; consider Y be object such that A3: Y in X by A2,XBOOLE_0:def 1; X is Subset of BoolePoset the carrier of L by Th3; then A4: "\/"(X,BoolePoset the carrier of L) = union X by YELLOW_1:21; then reconsider uX = union X as Subset of L by WAYBEL_8:26; reconsider Y as set by TARSKI:1; Y is Ideal of L by A3,YELLOW_2:41; then Bottom L in Y by WAYBEL_4:21; then reconsider uX as non empty Subset of L by A3,TARSKI:def 4; now let z be object; assume z in X; then z is Ideal of L by YELLOW_2:41; hence z in bool the carrier of L; end; then A5: X c= bool the carrier of L; A6: now let Y,Z be Subset of L; assume A7: Y in X & Z in X; then reconsider Y9 = Y, Z9 = Z as Element of InIdL; consider V9 be Element of InIdL such that A8: V9 in X and A9: Y9 <= V9 & Z9 <= V9 by A7,WAYBEL_0:def 1; reconsider V = V9 as Subset of L by YELLOW_2:41; take V; thus V in X by A8; Y9 "\/" Z9 <= V9 by A9,YELLOW_0:22; then A10: Y9 "\/" Z9 c= V9 by YELLOW_1:3; Y \/ Z c= Y9 "\/" Z9 by YELLOW_1:6; hence Y \/ Z c= V by A10; end; ( for Y be Subset of L st Y in X holds Y is lower)& for Y be Subset of L st Y in X holds Y is directed by YELLOW_2:41; then uX is Ideal of L by A5,A6,WAYBEL_0:26,46; then "\/"(X,BoolePoset the carrier of L) is Element of InIdL by A4, YELLOW_2:41; hence thesis; end; for X be Subset of InIdL st ex_inf_of X,BoolePoset the carrier of L holds "/\"(X,BoolePoset the carrier of L) in the carrier of InIdL proof let X be Subset of InIdL; assume ex_inf_of X,BoolePoset the carrier of L; now per cases; suppose A11: X is non empty; X is Subset of BoolePoset the carrier of L by Th3; then A12: "/\"(X,BoolePoset the carrier of L) = meet X by A11,YELLOW_1:20; InclPoset Ids L = RelStr (# Ids L, RelIncl Ids L #) by YELLOW_1:def 1; then "/\"(X,BoolePoset the carrier of L) is Ideal of L by A11,A12, YELLOW_2:45; then "/\"(X,BoolePoset the carrier of L) is Element of InIdL by YELLOW_2:41; hence thesis; end; suppose A13: X is empty; "/\"({},BoolePoset the carrier of L) = Top (BoolePoset the carrier of L ) by YELLOW_0:def 12 .= the carrier of L by YELLOW_1:19; then "/\"({},BoolePoset the carrier of L) is Ideal of L by Th4; then "/\"(X,BoolePoset the carrier of L) is Element of InIdL by A13, YELLOW_2:41; hence thesis; end; end; hence thesis; end; hence thesis by A1,WAYBEL_0:def 4,YELLOW_0:def 18; end; registration let L be non empty reflexive transitive RelStr; cluster principal for Ideal of L; existence proof set x = the Element of L; take downarrow x; thus thesis by WAYBEL_0:48; end; end; theorem Th9: for L be lower-bounded sup-Semilattice for X be non empty directed Subset of InclPoset Ids L holds sup X = union X proof let L be lower-bounded sup-Semilattice; let X be non empty directed Subset of InclPoset Ids L; consider z be object such that A1: z in X by XBOOLE_0:def 1; X c= the carrier of InclPoset Ids L; then A2: X c= Ids L by YELLOW_1:1; now let x be object; assume x in X; then x in Ids L by A2; then x in the set of all Y where Y is Ideal of L by WAYBEL_0:def 23; then ex x1 be Ideal of L st x = x1; hence x in bool the carrier of L; end; then A3: X c= bool the carrier of L; now let Z be Subset of L; assume Z in X; then Z in Ids L by A2; then Z in the set of all Y where Y is Ideal of L by WAYBEL_0:def 23; then ex Z1 be Ideal of L st Z = Z1; hence Z is lower; end; then reconsider unX = union X as lower Subset of L by A3,WAYBEL_0:26; reconsider z as set by TARSKI:1; z in Ids L by A2,A1; then z in the set of all Y where Y is Ideal of L by WAYBEL_0:def 23; then ex z1 be Ideal of L st z = z1; then ex v be object st v in z by XBOOLE_0:def 1; then reconsider unX as lower non empty Subset of L by A1,TARSKI:def 4; A4: now let V,Y be Subset of L; assume A5: V in X & Y in X; then reconsider V1 = V, Y1 = Y as Element of InclPoset Ids L; consider Z1 be Element of InclPoset Ids L such that A6: Z1 in X and A7: V1 <= Z1 & Y1 <= Z1 by A5,WAYBEL_0:def 1; Z1 in Ids L by A2,A6; then Z1 in the set of all Y9 where Y9 is Ideal of L by WAYBEL_0:def 23; then ex Z2 be Ideal of L st Z1 = Z2; then reconsider Z = Z1 as Subset of L; take Z; thus Z in X by A6; V c= Z & Y c= Z by A7,YELLOW_1:3; hence V \/ Y c= Z by XBOOLE_1:8; end; now let Z be Subset of L; assume Z in X; then Z in Ids L by A2; then Z in the set of all Y where Y is Ideal of L by WAYBEL_0:def 23; then ex Z1 be Ideal of L st Z = Z1; hence Z is directed; end; then reconsider unX as directed lower non empty Subset of L by A3,A4, WAYBEL_0:46; reconsider unX as Element of InclPoset Ids L by YELLOW_2:41; now let Y be set; assume A8: Y in X; then reconsider Y9 = Y as Element of InclPoset Ids L; sup X is_>=_than X by YELLOW_0:32; then Y9 <= sup X by A8,LATTICE3:def 9; hence Y c= sup X by YELLOW_1:3; end; then union X c= sup X by ZFMISC_1:76; then A9: unX <= sup X by YELLOW_1:3; for b be Element of InclPoset Ids L st b in X holds b <= unX by YELLOW_1:3,ZFMISC_1:74; then unX is_>=_than X by LATTICE3:def 9; then sup X <= unX by YELLOW_0:32; hence thesis by A9,ORDERS_2:2; end; theorem Th10: :: PROPOSITION 4.12.(i) for S be lower-bounded sup-Semilattice holds InclPoset Ids S is algebraic proof let S be lower-bounded sup-Semilattice; set BS = BoolePoset (the carrier of S); Ids S c= bool the carrier of S proof let x be object; assume x in Ids S; then x in the set of all X where X is Ideal of S by WAYBEL_0:def 23; then ex x1 be Ideal of S st x = x1; hence thesis; end; then reconsider InIdsS = InclPoset Ids S as non empty full SubRelStr of BoolePoset (the carrier of S) by YELLOW_1:5; A1: the carrier of InIdsS c= the carrier of BS by YELLOW_0:def 13; now let X be Subset of InIdsS; assume ex_inf_of X,BS; now per cases; suppose A2: X <> {}; for x being object st x in X holds x in the carrier of BS by A1; then X c= the carrier of BS; then "/\"(X,BS) = meet X by A2,YELLOW_1:20 .= "/\"(X,InIdsS) by A2,YELLOW_2:46; hence "/\"(X,BS) in the carrier of InIdsS; end; suppose A3: X = {}; "/\"({},BS) = Top BS by YELLOW_0:def 12 .= the carrier of S by YELLOW_1:19 .= [#]S .= "/\"({},InIdsS) by YELLOW_2:47; hence "/\"(X,BS) in the carrier of InIdsS by A3; end; end; hence "/\"(X,BS) in the carrier of InIdsS; end; then A4: InIdsS is infs-inheriting by YELLOW_0:def 18; now let Y be directed Subset of InIdsS; assume that A5: Y <> {} and ex_sup_of Y,BS; for x being object st x in Y holds x in the carrier of BS by A1; then Y c= the carrier of BS; then "\/"(Y,BS) = union Y by YELLOW_1:21 .= "\/"(Y,InIdsS) by A5,Th9; hence "\/"(Y,BS) in the carrier of InIdsS; end; then InIdsS is directed-sups-inheriting by WAYBEL_0:def 4; hence thesis by A4,Th6; end; theorem Th11: :: PROPOSITION 4.12.(i) for S be lower-bounded sup-Semilattice for x be Element of InclPoset Ids S holds x is compact iff x is principal Ideal of S proof let S be lower-bounded sup-Semilattice; reconsider InIdS = InclPoset Ids S as CLSubFrame of BoolePoset the carrier of S by Th8; let x be Element of InclPoset Ids S; reconsider x9 = x as Ideal of S by YELLOW_2:41; thus x is compact implies x is principal Ideal of S proof assume x is compact; then x in the carrier of CompactSublatt InIdS by WAYBEL_8:def 1; then consider F be Element of BoolePoset the carrier of S such that A1: F is finite and A2: x = meet { Y where Y is Element of InIdS : F c= Y } and A3: F c= x by Th7; A4: F c= the carrier of S by WAYBEL_8:26; ex y be Element of S st y in x9 & y is_>=_than x9 proof reconsider F9 = F as Subset of S by WAYBEL_8:26; reconsider F9 as Subset of S; reconsider y = sup F9 as Element of S; take y; now per cases; suppose F9 <> {}; hence y in x9 by A1,A3,WAYBEL_0:42; end; suppose F9 = {}; then y = Bottom S by YELLOW_0:def 11; hence y in x9 by WAYBEL_4:21; end; end; hence y in x9; now now let u be object; assume A5: u in F; then reconsider u9 = u as Element of S by A4; ex_sup_of F9,S by A1,A5,YELLOW_0:54; then y is_>=_than F by YELLOW_0:30; then u9 <= y by A5,LATTICE3:def 9; hence u in downarrow y by WAYBEL_0:17; end; then A6: F c= downarrow y; let b be Element of S; assume A7: b in x9; downarrow y is Element of InIdS by YELLOW_2:41; then downarrow y in { Y where Y is Element of InIdS : F c= Y } by A6; then b in downarrow y by A2,A7,SETFAM_1:def 1; hence b <= y by WAYBEL_0:17; end; hence thesis by LATTICE3:def 9; end; hence thesis by WAYBEL_0:def 21; end; thus x is principal Ideal of S implies x is compact proof assume x is principal Ideal of S; then consider y be Element of S such that A8: y in x9 and A9: y is_>=_than x9 by WAYBEL_0:def 21; ex F be Element of BoolePoset the carrier of S st F is finite & F c= x & x = meet { Y where Y is Element of InIdS : F c= Y } proof reconsider F = {y} as Element of BoolePoset the carrier of S by WAYBEL_8:26; take F; thus F is finite; for v be object st v in F holds v in x by A8,TARSKI:def 1; hence A10: F c= x; A11: now let z be object; thus z in x implies for Z be set holds Z in { Y where Y is Element of InIdS: F c= Y } implies z in Z proof assume A12: z in x; then reconsider z9 = z as Element of S by YELLOW_2:42; A13: z9 <= y by A9,A12,LATTICE3:def 9; let Z be set; assume Z in { Y where Y is Element of InIdS : F c= Y }; then consider Z1 be Element of InIdS such that A14: Z1 = Z & F c= Z1; Z1 is Ideal of S & y in F by TARSKI:def 1,YELLOW_2:41; hence thesis by A14,A13,WAYBEL_0:def 19; end; thus ( for Z be set holds Z in { Y where Y is Element of InIdS : F c= Y } implies z in Z ) implies z in x proof assume A15: for Z be set holds Z in { Y where Y is Element of InIdS : F c= Y } implies z in Z; x in { Y where Y is Element of InIdS : F c= Y } by A10; hence thesis by A15; end; end; [#]S is Element of InIdS by YELLOW_2:41; then [#]S in { Y where Y is Element of InIdS : F c= Y }; hence thesis by A11,SETFAM_1:def 1; end; then x in the carrier of CompactSublatt InIdS by Th7; hence thesis by WAYBEL_8:def 1; end; end; theorem Th12: for S be lower-bounded sup-Semilattice for x be Element of InclPoset Ids S holds x is compact iff ex a be Element of S st x = downarrow a proof let S be lower-bounded sup-Semilattice; let x be Element of InclPoset Ids S; thus x is compact implies ex a be Element of S st x = downarrow a proof assume x is compact; then x is principal Ideal of S by Th11; hence thesis by WAYBEL_0:48; end; thus (ex a be Element of S st x = downarrow a) implies x is compact by WAYBEL_0:48,Th11; end; theorem :: PROPOSITION 4.12.(ii) for L be lower-bounded sup-Semilattice for f be Function of L, CompactSublatt InclPoset Ids L st for x be Element of L holds f.x = downarrow x holds f is isomorphic proof let L be lower-bounded sup-Semilattice; let f be Function of L, CompactSublatt InclPoset Ids L; assume A1: for x be Element of L holds f.x = downarrow x; A2: for x,y be Element of L holds x <= y iff f.x <= f.y proof let x,y be Element of L; reconsider fx = f.x as Element of InclPoset Ids L by YELLOW_0:58; reconsider fy = f.y as Element of InclPoset Ids L by YELLOW_0:58; thus x <= y implies f.x <= f.y proof assume x <= y; then downarrow x c= downarrow y by WAYBEL_0:21; then f.x c= downarrow y by A1; then fx c= fy by A1; then fx <= fy by YELLOW_1:3; hence thesis by YELLOW_0:60; end; x <= x; then A3: x in downarrow x by WAYBEL_0:17; thus f.x <= f.y implies x <= y proof assume f.x <= f.y; then fx <= fy by YELLOW_0:59; then fx c= fy by YELLOW_1:3; then f.x c= downarrow y by A1; then downarrow x c= downarrow y by A1; hence thesis by A3,WAYBEL_0:17; end; end; now let y be object; assume A4: y in the carrier of CompactSublatt InclPoset Ids L; the carrier of CompactSublatt InclPoset Ids L c= the carrier of InclPoset Ids L by YELLOW_0:def 13; then reconsider y9 = y as Element of InclPoset Ids L by A4; y9 is compact by A4,WAYBEL_8:def 1; then consider x be Element of L such that A5: y9 = downarrow x by Th12; reconsider x9 = x as object; take x9; thus x9 in the carrier of L; thus y = f.x9 by A1,A5; end; then A6: rng f = the carrier of CompactSublatt InclPoset Ids L by FUNCT_2:10; now let x,y be Element of L; assume f.x = f.y; then f.x = downarrow y by A1; then downarrow x = downarrow y by A1; hence x = y by WAYBEL_0:19; end; then f is one-to-one by WAYBEL_1:def 1; hence thesis by A6,A2,WAYBEL_0:66; end; theorem :: PROPOSITION 4.12.(iii) for S be lower-bounded LATTICE holds InclPoset Ids S is arithmetic proof let S be lower-bounded LATTICE; now let x,y be Element of CompactSublatt InclPoset Ids S; reconsider x1 = x, y1 = y as Element of InclPoset Ids S by YELLOW_0:58; x1 is compact by WAYBEL_8:def 1; then consider a be Element of S such that A1: x1 = downarrow a by Th12; y1 is compact by WAYBEL_8:def 1; then consider b be Element of S such that A2: y1 = downarrow b by Th12; Bottom S <= b by YELLOW_0:44; then A3: Bottom S in downarrow b by WAYBEL_0:17; Bottom S <= a by YELLOW_0:44; then Bottom S in downarrow a by WAYBEL_0:17; then reconsider xy = downarrow a /\ downarrow b as non empty Subset of S by A3, XBOOLE_0:def 4; reconsider xy as lower non empty Subset of S by WAYBEL_0:27; reconsider xy as lower directed non empty Subset of S by WAYBEL_0:44; xy is Ideal of S; then downarrow a /\ downarrow b in the set of all X where X is Ideal of S; then downarrow a /\ downarrow b in Ids S by WAYBEL_0:def 23; then x1 "/\" y1 = downarrow a /\ downarrow b by A1,A2,YELLOW_1:9; then reconsider z1 = downarrow a /\ downarrow b as Element of InclPoset Ids S; z1 c= y1 by A2,XBOOLE_1:17; then A4: z1 <= y1 by YELLOW_1:3; A5: downarrow (a "/\" b) c= downarrow a /\ downarrow b proof let v be object; assume A6: v in downarrow (a "/\" b); then reconsider v1 = v as Element of S; A7: v1 <= a "/\" b by A6,WAYBEL_0:17; a "/\" b <= b by YELLOW_0:23; then v1 <= b by A7,ORDERS_2:3; then A8: v in downarrow b by WAYBEL_0:17; a "/\" b <= a by YELLOW_0:23; then v1 <= a by A7,ORDERS_2:3; then v in downarrow a by WAYBEL_0:17; hence thesis by A8,XBOOLE_0:def 4; end; downarrow a /\ downarrow b c= downarrow (a "/\" b) proof let v be object; assume A9: v in downarrow a /\ downarrow b; then reconsider v1 = v as Element of S; v in downarrow b by A9,XBOOLE_0:def 4; then A10: v1 <= b by WAYBEL_0:17; v in downarrow a by A9,XBOOLE_0:def 4; then v1 <= a by WAYBEL_0:17; then v1 <= a "/\" b by A10,YELLOW_0:23; hence thesis by WAYBEL_0:17; end; then z1 = downarrow (a "/\" b) by A5,XBOOLE_0:def 10; then z1 is compact by Th12; then reconsider z = z1 as Element of CompactSublatt InclPoset Ids S by WAYBEL_8:def 1; take z; z1 c= x1 by A1,XBOOLE_1:17; then z1 <= x1 by YELLOW_1:3; hence z <= x & z <= y by A4,YELLOW_0:60; let v be Element of CompactSublatt InclPoset Ids S; reconsider v1 = v as Element of InclPoset Ids S by YELLOW_0:58; assume that A11: v <= x and A12: v <= y; v1 <= y1 by A12,YELLOW_0:59; then A13: v1 c= y1 by YELLOW_1:3; v1 <= x1 by A11,YELLOW_0:59; then v1 c= x1 by YELLOW_1:3; then v1 c= z1 by A1,A2,A13,XBOOLE_1:19; then v1 <= z1 by YELLOW_1:3; hence v <= z by YELLOW_0:60; end; then A14: CompactSublatt InclPoset Ids S is with_infima by LATTICE3:def 11; InclPoset Ids S is algebraic by Th10; hence thesis by A14,WAYBEL_8:19; end; theorem Th15: :: PROPOSITION 4.12.(iv) for L be lower-bounded sup-Semilattice holds CompactSublatt L is lower-bounded sup-Semilattice proof let L be lower-bounded sup-Semilattice; ex x being Element of CompactSublatt L st x is_<=_than the carrier of CompactSublatt L proof reconsider x = Bottom L as Element of CompactSublatt L by WAYBEL_8:3; take x; now let a be Element of CompactSublatt L; A1: the carrier of CompactSublatt L c= the carrier of L by YELLOW_0:def 13; assume a in the carrier of CompactSublatt L; reconsider a9 = a as Element of L by A1; Bottom L <= a9 by YELLOW_0:44; hence x <= a by YELLOW_0:60; end; hence thesis by LATTICE3:def 8; end; hence thesis by YELLOW_0:def 4; end; theorem Th16: :: PROPOSITION 4.12.(v) for L be algebraic lower-bounded sup-Semilattice for f be Function of L,InclPoset Ids CompactSublatt L st for x be Element of L holds f.x = compactbelow x holds f is isomorphic proof let L be algebraic lower-bounded sup-Semilattice; let f be Function of L,InclPoset Ids CompactSublatt L; assume A1: for x be Element of L holds f.x = compactbelow x; A2: now let x,y be Element of L; thus x <= y implies f.x <= f.y proof assume x <= y; then compactbelow x c= compactbelow y by Th1; then f.x c= compactbelow y by A1; then f.x c= f.y by A1; hence thesis by YELLOW_1:3; end; thus f.x <= f.y implies x <= y proof assume f.x <= f.y; then f.x c= f.y by YELLOW_1:3; then f.x c= compactbelow y by A1; then A3: compactbelow x c= compactbelow y by A1; ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L by YELLOW_0:17; then sup compactbelow x <= sup compactbelow y by A3,YELLOW_0:34; then sup compactbelow x <= y by WAYBEL_8:def 3; hence thesis by WAYBEL_8:def 3; end; end; now let y be object; assume y in the carrier of InclPoset Ids CompactSublatt L; then reconsider y9 = y as Ideal of CompactSublatt L by YELLOW_2:41; reconsider y1 = y9 as non empty Subset of L by Th3; reconsider y1 as non empty directed Subset of L by YELLOW_2:7; set x = sup y1; reconsider x9 = x as object; take x9; thus x9 in the carrier of L; A4: compactbelow x c= y9 proof let d be object; assume d in compactbelow x; then d in {v where v is Element of L: x >= v & v is compact} by WAYBEL_8:def 2; then consider d1 be Element of L such that A5: d1 = d and A6: d1 <= x and A7: d1 is compact; reconsider d9 = d1 as Element of CompactSublatt L by A7,WAYBEL_8:def 1; d1 << d1 by A7,WAYBEL_3:def 2; then consider z be Element of L such that A8: z in y1 and A9: d1 <= z by A6,WAYBEL_3:def 1; reconsider z9 = z as Element of CompactSublatt L by A8; d9 <= z9 by A9,YELLOW_0:60; hence thesis by A5,A8,WAYBEL_0:def 19; end; y9 c= compactbelow x proof let d be object; assume A10: d in y9; then reconsider d1 = d as Element of CompactSublatt L; reconsider d9 = d1 as Element of L by YELLOW_0:58; y9 is_<=_than sup y1 by YELLOW_0:32; then d9 is compact & d9 <= x by A10,LATTICE3:def 9,WAYBEL_8:def 1; hence thesis by WAYBEL_8:4; end; hence y = compactbelow x by A4,XBOOLE_0:def 10 .= f.x9 by A1; end; then A11: rng f = the carrier of InclPoset Ids CompactSublatt L by FUNCT_2:10; now let x,y be Element of L; assume f.x = f.y; then f.x = compactbelow y by A1; then compactbelow x = compactbelow y by A1; then sup compactbelow x = y by WAYBEL_8:def 3; hence x = y by WAYBEL_8:def 3; end; then f is one-to-one by WAYBEL_1:def 1; hence thesis by A11,A2,WAYBEL_0:66; end; theorem :: PROPOSITION 4.12.(vi) for L be algebraic lower-bounded sup-Semilattice for x be Element of L holds compactbelow x is principal Ideal of CompactSublatt L iff x is compact proof let L be algebraic lower-bounded sup-Semilattice; let x be Element of L; thus compactbelow x is principal Ideal of CompactSublatt L implies x is compact proof assume compactbelow x is principal Ideal of CompactSublatt L; then consider y be Element of CompactSublatt L such that A1: y in compactbelow x and A2: y is_>=_than compactbelow x by WAYBEL_0:def 21; reconsider y9 = y as Element of L by YELLOW_0:58; compactbelow x is Subset of CompactSublatt L by Th2; then y9 is_>=_than compactbelow x by A2,YELLOW_0:62; then y9 >= sup compactbelow x by YELLOW_0:32; then A3: x <= y9 by WAYBEL_8:def 3; y9 <= x & y9 is compact by A1,WAYBEL_8:4; hence thesis by A3,ORDERS_2:2; end; thus x is compact implies compactbelow x is principal Ideal of CompactSublatt L proof reconsider I = compactbelow x as non empty Subset of CompactSublatt L by Th2; assume A4: x is compact; then reconsider x9 = x as Element of CompactSublatt L by WAYBEL_8:def 1; compactbelow x is non empty directed Subset of L by WAYBEL_8:def 4; then reconsider I as non empty directed Subset of CompactSublatt L by WAYBEL10:23; now let y,z be Element of CompactSublatt L; reconsider y9 = y, z9 = z as Element of L by YELLOW_0:58; assume y in I & z <= y; then y9 <= x & z9 <= y9 by WAYBEL_8:4,YELLOW_0:59; then A5: z9 <= x by ORDERS_2:3; z9 is compact by WAYBEL_8:def 1; hence z in I by A5,WAYBEL_8:4; end; then reconsider I as Ideal of CompactSublatt L by WAYBEL_0:def 19; sup compactbelow x is_>=_than compactbelow x by YELLOW_0:32; then x is_>=_than I by WAYBEL_8:def 3; then A6: x9 is_>=_than I by YELLOW_0:61; x <= x; then x9 in I by A4,WAYBEL_8:4; hence thesis by A6,WAYBEL_0:def 21; end; end; begin :: Maps theorem Th18: for L1,L2 be non empty RelStr for X be Subset of L1, x be Element of L1 for f be Function of L1,L2 st f is isomorphic holds x is_<=_than X iff f.x is_<=_than f.:X proof let L1,L2 be non empty RelStr; let X be Subset of L1; let x be Element of L1; let f be Function of L1,L2; assume A1: f is isomorphic; hence x is_<=_than X implies f.x is_<=_than f.:X by YELLOW_2:13; thus f.x is_<=_than f.:X implies x is_<=_than X proof reconsider g = f" as Function of L2,L1 by A1,WAYBEL_0:67; assume A2: f.x is_<=_than f.:X; g is isomorphic by A1,WAYBEL_0:68; then A3: g.(f.x) is_<=_than g.:(f.:X) by A2,YELLOW_2:13; A4: f"(f.:X) c= X by A1,FUNCT_1:82; X c= the carrier of L1; then X c= dom f by FUNCT_2:def 1; then A5: X c= f"(f.:X) by FUNCT_1:76; x in the carrier of L1; then A6: x in dom f by FUNCT_2:def 1; g.:(f.:X) = f"(f.:X) by A1,FUNCT_1:85 .= X by A4,A5,XBOOLE_0:def 10; hence thesis by A1,A6,A3,FUNCT_1:34; end; end; theorem Th19: for L1,L2 be non empty RelStr for X be Subset of L1, x be Element of L1 for f be Function of L1,L2 st f is isomorphic holds x is_>=_than X iff f.x is_>=_than f.:X proof let L1,L2 be non empty RelStr; let X be Subset of L1; let x be Element of L1; let f be Function of L1,L2; assume A1: f is isomorphic; hence x is_>=_than X implies f.x is_>=_than f.:X by YELLOW_2:14; thus f.x is_>=_than f.:X implies x is_>=_than X proof reconsider g = f" as Function of L2,L1 by A1,WAYBEL_0:67; assume A2: f.x is_>=_than f.:X; g is isomorphic by A1,WAYBEL_0:68; then A3: g.(f.x) is_>=_than g.:(f.:X) by A2,YELLOW_2:14; A4: f"(f.:X) c= X by A1,FUNCT_1:82; X c= the carrier of L1; then X c= dom f by FUNCT_2:def 1; then A5: X c= f"(f.:X) by FUNCT_1:76; x in the carrier of L1; then A6: x in dom f by FUNCT_2:def 1; g.:(f.:X) = f"(f.:X) by A1,FUNCT_1:85 .= X by A4,A5,XBOOLE_0:def 10; hence thesis by A1,A6,A3,FUNCT_1:34; end; end; theorem Th20: for L1,L2 be non empty antisymmetric RelStr for f be Function of L1,L2 holds f is isomorphic implies f is infs-preserving sups-preserving proof let L1,L2 be non empty antisymmetric RelStr; let f be Function of L1,L2; assume A1: f is isomorphic; then A2: rng f = the carrier of L2 by WAYBEL_0:66; now let X be Subset of L1; now assume A3: ex_inf_of X,L1; then consider a be Element of L1 such that A4: X is_>=_than a and A5: for b be Element of L1 st X is_>=_than b holds a >= b by YELLOW_0:16; A6: now let c be Element of L2; consider e be object such that A7: e in dom f and A8: c = f.e by A2,FUNCT_1:def 3; reconsider e as Element of L1 by A7; assume f.:X is_>=_than c; then X is_>=_than e by A1,A8,Th18; then a >= e by A5; hence f.a >= c by A1,A8,WAYBEL_0:66; end; f.:X is_>=_than f.a by A1,A4,Th18; hence ex_inf_of f.:X,L2 by A6,YELLOW_0:16; A9: now let b be Element of L2; consider v be object such that A10: v in dom f and A11: b = f.v by A2,FUNCT_1:def 3; reconsider v as Element of L1 by A10; assume b is_<=_than f.:X; then v is_<=_than X by A1,A11,Th18; then inf X >= v by A3,YELLOW_0:31; hence f.inf X >= b by A1,A11,WAYBEL_0:66; end; inf X is_<=_than X by A3,YELLOW_0:31; then f.inf X is_<=_than f.:X by A1,Th18; hence inf (f.:X) = f.inf X by A9,YELLOW_0:31; end; hence f preserves_inf_of X by WAYBEL_0:def 30; end; hence f is infs-preserving by WAYBEL_0:def 32; now let X be Subset of L1; now assume A12: ex_sup_of X,L1; then consider a be Element of L1 such that A13: X is_<=_than a and A14: for b be Element of L1 st X is_<=_than b holds a <= b by YELLOW_0:15; A15: now let c be Element of L2; consider e be object such that A16: e in dom f and A17: c = f.e by A2,FUNCT_1:def 3; reconsider e as Element of L1 by A16; assume f.:X is_<=_than c; then X is_<=_than e by A1,A17,Th19; then a <= e by A14; hence f.a <= c by A1,A17,WAYBEL_0:66; end; f.:X is_<=_than f.a by A1,A13,Th19; hence ex_sup_of f.:X,L2 by A15,YELLOW_0:15; A18: now let b be Element of L2; consider v be object such that A19: v in dom f and A20: b = f.v by A2,FUNCT_1:def 3; reconsider v as Element of L1 by A19; assume b is_>=_than f.:X; then v is_>=_than X by A1,A20,Th19; then sup X <= v by A12,YELLOW_0:30; hence f.sup X <= b by A1,A20,WAYBEL_0:66; end; sup X is_>=_than X by A12,YELLOW_0:30; then f.sup X is_>=_than f.:X by A1,Th19; hence sup (f.:X) = f.sup X by A18,YELLOW_0:30; end; hence f preserves_sup_of X by WAYBEL_0:def 31; end; hence thesis by WAYBEL_0:def 33; end; registration let L1,L2 be non empty antisymmetric RelStr; cluster isomorphic -> infs-preserving sups-preserving for Function of L1,L2; coherence by Th20; end; theorem Th21: for L1,L2,L3 be non empty transitive antisymmetric RelStr for f be Function of L1,L2 st f is infs-preserving holds L2 is full infs-inheriting SubRelStr of L3 & L3 is complete implies ex g be Function of L1,L3 st f = g & g is infs-preserving proof let L1,L2,L3 be non empty transitive antisymmetric RelStr; let f be Function of L1,L2; assume that A1: f is infs-preserving and A2: L2 is full infs-inheriting SubRelStr of L3 and A3: L3 is complete; the carrier of L2 c= the carrier of L3 by A2,YELLOW_0:def 13; then reconsider g = f as Function of L1,L3 by FUNCT_2:7; take g; thus f = g; now let X be Subset of L1; now A4: f preserves_inf_of X by A1,WAYBEL_0:def 32; assume A5: ex_inf_of X,L1; thus A6: ex_inf_of g.:X,L3 by A3,YELLOW_0:17; then "/\"(f.:X,L3) in the carrier of L2 by A2,YELLOW_0:def 18; hence inf (g.:X) = inf (f.:X) by A2,A6,YELLOW_0:63 .= g.inf X by A5,A4,WAYBEL_0:def 30; end; hence g preserves_inf_of X by WAYBEL_0:def 30; end; hence thesis by WAYBEL_0:def 32; end; theorem Th22: for L1,L2,L3 be non empty transitive antisymmetric RelStr for f be Function of L1,L2 st f is monotone directed-sups-preserving holds L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete implies ex g be Function of L1,L3 st f = g & g is directed-sups-preserving proof let L1,L2,L3 be non empty transitive antisymmetric RelStr; let f be Function of L1,L2; assume that A1: f is monotone directed-sups-preserving and A2: L2 is full directed-sups-inheriting SubRelStr of L3 and A3: L3 is complete; the carrier of L2 c= the carrier of L3 by A2,YELLOW_0:def 13; then reconsider g = f as Function of L1,L3 by FUNCT_2:7; take g; thus f = g; now let X be Subset of L1; assume A4: X is non empty directed; then consider d be object such that A5: d in X by XBOOLE_0:def 1; d in the carrier of L1 by A5; then d in dom f by FUNCT_2:def 1; then f.d in f.:X by A5,FUNCT_1:def 6; then A6: f.:X is non empty directed by A1,A4,YELLOW_2:15; now A7: f preserves_sup_of X by A1,A4,WAYBEL_0:def 37; assume A8: ex_sup_of X,L1; thus ex_sup_of g.:X,L3 by A3,YELLOW_0:17; hence sup (g.:X) = sup (f.:X) by A2,A6,WAYBEL_0:7 .= g.sup X by A8,A7,WAYBEL_0:def 31; end; hence g preserves_sup_of X by WAYBEL_0:def 31; end; hence thesis by WAYBEL_0:def 37; end; theorem Th23: for L be lower-bounded sup-Semilattice holds InclPoset Ids CompactSublatt L is CLSubFrame of BoolePoset the carrier of CompactSublatt L proof let L be lower-bounded sup-Semilattice; CompactSublatt L is lower-bounded sup-Semilattice by Th15; hence thesis by Th8; end; theorem Th24: :: COROLLARY 4.13. for L be algebraic lower-bounded LATTICE ex g be Function of L, BoolePoset the carrier of CompactSublatt L st g is infs-preserving & g is directed-sups-preserving & g is one-to-one & for x be Element of L holds g.x = compactbelow x proof let L be algebraic lower-bounded LATTICE; deffunc F(Element of L) = compactbelow \$1; A1: for y be Element of L holds F(y) is Element of InclPoset Ids CompactSublatt L proof let y be Element of L; reconsider comy = compactbelow y as non empty directed Subset of L by WAYBEL_8:def 4; reconsider comy as non empty Subset of CompactSublatt L by Th2; reconsider comy as non empty directed Subset of CompactSublatt L by WAYBEL10:23; now let x1,z1 be Element of CompactSublatt L; reconsider x2 = x1, z2 = z1 as Element of L by YELLOW_0:58; assume x1 in comy & z1 <= x1; then x2 <= y & z2 <= x2 by WAYBEL_8:4,YELLOW_0:59; then A2: z2 <= y by ORDERS_2:3; z2 is compact by WAYBEL_8:def 1; hence z1 in comy by A2,WAYBEL_8:4; end; then comy is lower by WAYBEL_0:def 19; hence thesis by YELLOW_2:41; end; consider g1 be Function of L, InclPoset Ids CompactSublatt L such that A3: for y be Element of L holds g1.y = F(y) from FUNCT_2:sch 9(A1); now let k be object; assume k in the carrier of InclPoset Ids CompactSublatt L; then k is Ideal of CompactSublatt L by YELLOW_2:41; then k is Element of BoolePoset the carrier of CompactSublatt L by WAYBEL_8:26; hence k in the carrier of BoolePoset the carrier of CompactSublatt L; end; then the carrier of InclPoset Ids CompactSublatt L c= the carrier of BoolePoset the carrier of CompactSublatt L; then reconsider g = g1 as Function of L,BoolePoset the carrier of CompactSublatt L by FUNCT_2:7; take g; A4: g1 is isomorphic by A3,Th16; A5: InclPoset Ids CompactSublatt L is full infs-inheriting directed-sups-inheriting SubRelStr of BoolePoset the carrier of CompactSublatt L by Th23; then ex g2 be Function of L,BoolePoset the carrier of CompactSublatt L st g1 = g2 & g2 is infs-preserving by A4,Th21; hence g is infs-preserving; ex g3 be Function of L,BoolePoset the carrier of CompactSublatt L st g1 = g3 & g3 is directed-sups-preserving by A4,A5,Th22; hence g is directed-sups-preserving; thus g is one-to-one by A4; let x be Element of L; thus thesis by A3; end; theorem :: PROPOSITION 4.14. for I be non empty set for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds J.i is algebraic lower-bounded LATTICE holds product J is algebraic lower-bounded LATTICE proof let I be non empty set; let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; assume A1: for i be Element of I holds J.i is algebraic lower-bounded LATTICE; then A2: for i be Element of I holds J.i is complete LATTICE; then reconsider L = product J as non empty lower-bounded LATTICE by WAYBEL_3:31; for i be Element of I holds J.i is antisymmetric by A1; then A3: product J is antisymmetric by WAYBEL_3:30; now let x be Element of product J; A4: for i be Element of I holds sup compactbelow (x.i) = (sup compactbelow x).i proof let i be Element of I; A5: compactbelow (x.i) c= pi(compactbelow x,i) proof deffunc G(Element of I) = Bottom (J.\$1); defpred C[set] means \$1 = i; let v be object; assume v in compactbelow (x.i); then v in {y where y is Element of J.i: x.i >= y & y is compact} by WAYBEL_8:def 2; then consider v1 be Element of J.i such that A6: v1 = v and A7: x.i >= v1 and A8: v1 is compact; deffunc F(set) = v1; consider f be Function such that A9: dom f = I and A10: for j be Element of I holds ( C[j] implies f.j = F(j) ) & ( not C[j] implies f.j = G(j)) from PARTFUN1:sch 4; A11: f.i = v1 by A10; now let k be Element of I; now per cases; suppose k = i; hence f.k is Element of J.k by A10; end; suppose k <> i; then f.k = Bottom (J.k) by A10; hence f.k is Element of J.k; end; end; hence f.k is Element of J.k; end; then reconsider f as Element of product J by A9,WAYBEL_3:27; now let k be Element of I; A12: J.k is algebraic lower-bounded LATTICE by A1; now per cases; suppose k = i; hence f.k <= x.k by A7,A10; end; suppose k <> i; then f.k = Bottom (J.k) by A10; hence f.k <= x.k by A12,YELLOW_0:44; end; end; hence f.k <= x.k; end; then A13: f <= x by WAYBEL_3:28; A14: now let k be Element of I; A15: J.k is algebraic lower-bounded LATTICE by A1; now per cases; suppose A16: k = i; then f.k = v1 by A10; hence f.k << f.k by A8,A16,WAYBEL_3:def 2; end; suppose k <> i; then f.k = Bottom (J.k) by A10; then f.k is compact by A15,WAYBEL_3:15; hence f.k << f.k by WAYBEL_3:def 2; end; end; hence f.k << f.k; end; ex K be finite Subset of I st for k be Element of I st not k in K holds f.k = Bottom (J.k) proof take K = {i}; let k be Element of I; assume not k in K; then k <> i by TARSKI:def 1; hence thesis by A10; end; then f << f by A2,A14,WAYBEL_3:33; then f is compact by WAYBEL_3:def 2; then f in compactbelow x by A13,WAYBEL_8:4; hence thesis by A6,A11,CARD_3:def 6; end; pi(compactbelow x,i) c= compactbelow (x.i) proof let v be object; assume v in pi(compactbelow x,i); then consider f be Function such that A17: f in compactbelow x and A18: v = f.i by CARD_3:def 6; f in {y where y is Element of product J: x >= y & y is compact} by A17,WAYBEL_8:def 2; then consider f1 be Element of product J such that A19: f1 = f and A20: x >= f1 and A21: f1 is compact; f1 << f1 by A21,WAYBEL_3:def 2; then f1.i << f1.i by A2,WAYBEL_3:33; then A22: f1.i is compact by WAYBEL_3:def 2; f1.i <= x.i by A20,WAYBEL_3:28; hence thesis by A18,A19,A22,WAYBEL_8:4; end; hence sup compactbelow (x.i) = sup pi(compactbelow x,i) by A5, XBOOLE_0:def 10 .= (sup compactbelow x).i by A2,WAYBEL_3:32; end; now let i be Element of I; J.i is satisfying_axiom_K by A1; then x.i = sup compactbelow (x.i) by WAYBEL_8:def 3; hence (sup compactbelow x).i <= x.i by A4; end; then A23: sup compactbelow x <= x by WAYBEL_3:28; now let i be Element of I; J.i is satisfying_axiom_K by A1; then x.i = sup compactbelow (x.i) by WAYBEL_8:def 3; hence x.i <= (sup compactbelow x).i by A4; end; then x <= sup compactbelow x by WAYBEL_3:28; hence x = sup compactbelow x by A3,A23,YELLOW_0:def 3; end; then A24: product J is satisfying_axiom_K by WAYBEL_8:def 3; A25: for x be Element of L holds compactbelow x is non empty directed proof let x be Element of L; now let c,d be Element of L; assume that A26: c in compactbelow x and A27: d in compactbelow x; d is compact by A27,WAYBEL_8:4; then d <= c "\/" d & d << d by WAYBEL_3:def 2,YELLOW_0:22; then A28: d << c "\/" d by WAYBEL_3:2; c is compact by A26,WAYBEL_8:4; then c <= c "\/" d & c << c by WAYBEL_3:def 2,YELLOW_0:22; then c << c "\/" d by WAYBEL_3:2; then c "\/" d << c "\/" d by A28,WAYBEL_3:3; then A29: c "\/" d is compact by WAYBEL_3:def 2; take e = c "\/" d; c <= x & d <= x by A26,A27,WAYBEL_8:4; then c "\/" d <= x by YELLOW_0:22; hence e in compactbelow x by A29,WAYBEL_8:4; thus c <= e & d <= e by YELLOW_0:22; end; hence thesis by WAYBEL_0:def 1; end; L is up-complete by A2,WAYBEL_3:31; hence thesis by A25,A24,WAYBEL_8:def 4; end; Lm1: for L be lower-bounded LATTICE holds L is algebraic implies ex X be non empty set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic proof let L be lower-bounded LATTICE; assume A1: L is algebraic; then reconsider L9 = L as algebraic lower-bounded LATTICE; take X = the carrier of CompactSublatt L; consider g be Function of L,BoolePoset the carrier of CompactSublatt L such that A2: g is infs-preserving and A3: g is directed-sups-preserving and A4: g is one-to-one and A5: for x be Element of L holds g.x = compactbelow x by A1,Th24; reconsider S = Image g as non empty full SubRelStr of BoolePoset X; take S; A6: L9 is complete; hence S is infs-inheriting by A2,YELLOW_2:33; A7: rng g = the carrier of S by YELLOW_0:def 15; dom g = the carrier of L by FUNCT_2:def 1; then reconsider g1 = g as Function of L,S by A7,FUNCT_2:1; now let x,y be Element of L; thus x <= y implies g1.x <= g1.y proof assume x <= y; then compactbelow x c= compactbelow y by Th1; then g.x c= compactbelow y by A5; then g.x c= g.y by A5; then g.x <= g.y by YELLOW_1:2; hence thesis by YELLOW_0:60; end; thus g1.x <= g1.y implies x <= y proof assume g1.x <= g1.y; then g.x <= g.y by YELLOW_0:59; then g.x c= g.y by YELLOW_1:2; then g.x c= compactbelow y by A5; then A8: compactbelow x c= compactbelow y by A5; ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L by A6,YELLOW_0:17 ; then sup compactbelow x <= sup compactbelow y by A8,YELLOW_0:34; then x <= sup compactbelow y by A1,WAYBEL_8:def 3; hence thesis by A1,WAYBEL_8:def 3; end; end; then A9: g1 is isomorphic by A4,A7,WAYBEL_0:66; then reconsider f1 = g1" as Function of S,L by WAYBEL_0:67; A10: f1 is isomorphic by A9,WAYBEL_0:68; now let Y be directed Subset of S; assume that A11: Y <> {} and ex_sup_of Y,BoolePoset X; now let X2 be finite Subset of f1.:Y; A12: g1"(g1.:X2) c= X2 by A4,FUNCT_1:82; now let v be object; assume v in g1.:X2; then ex u be object st u in dom g1 & u in X2 & v = g1.u by FUNCT_1:def 6; then v in g1.:(f1.:Y) by FUNCT_1:def 6; then v in g1.:(g1"Y) by A4,FUNCT_1:85; hence v in Y by A7,FUNCT_1:77; end; then reconsider Y1 = g1.:X2 as finite Subset of Y by TARSKI:def 3; consider y1 be Element of S such that A13: y1 in Y and A14: y1 is_>=_than Y1 by A11,WAYBEL_0:1; take f1y1 = f1.y1; y1 in the carrier of S; then y1 in dom f1 by FUNCT_2:def 1; hence f1y1 in f1.:Y by A13,FUNCT_1:def 6; X2 c= the carrier of L by XBOOLE_1:1; then X2 c= dom g1 by FUNCT_2:def 1; then A15: X2 c= g1"(g1.:X2) by FUNCT_1:76; f1.:Y1 = g1"(g1.:X2) by A4,FUNCT_1:85 .= X2 by A15,A12,XBOOLE_0:def 10; hence f1y1 is_>=_than X2 by A10,A14,Th19; end; then reconsider X1 = f1.:Y as non empty directed Subset of L by WAYBEL_0:1; sup X1 in the carrier of L; then sup X1 in dom g by FUNCT_2:def 1; then A16: g.sup X1 in rng g by FUNCT_1:def 3; ex_sup_of X1,L & g preserves_sup_of X1 by A6,A3,WAYBEL_0:def 37,YELLOW_0:17 ; then A17: sup (g.:X1) in rng g by A16,WAYBEL_0:def 31; g.:X1 = g.:(g1"Y) by A4,FUNCT_1:85 .= Y by A7,FUNCT_1:77; hence "\/"(Y,BoolePoset X) in the carrier of S by A17,YELLOW_0:def 15; end; hence S is directed-sups-inheriting by WAYBEL_0:def 4; thus thesis by A9,WAYBEL_1:def 8; end; theorem Th26: for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 holds L1,L2 are_isomorphic proof let L1,L2 be non empty RelStr; assume A1: the RelStr of L1 = the RelStr of L2; ex f be Function of L1,L2 st f is isomorphic proof reconsider f = id the carrier of L1 as Function of L1,L2 by A1; take f; now let z be object; assume A2: z in the carrier of L2; take v = z; thus v in the carrier of L1 by A1,A2; thus z = f.v by A1,A2,FUNCT_1:18; end; then A3: rng f = the carrier of L2 by FUNCT_2:10; for x,y be Element of L1 holds x <= y iff f.x <= f.y by A1,YELLOW_0:1; hence thesis by A3,WAYBEL_0:66; end; hence thesis by WAYBEL_1:def 8; end; Lm2: for L be LATTICE holds (ex X be non empty set, S be full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )) implies ex X be non empty set, c be closure Function of BoolePoset X,BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic proof let L be LATTICE; given X be non empty set, S be full SubRelStr of BoolePoset X such that A1: S is infs-inheriting and A2: S is directed-sups-inheriting and A3: L,S are_isomorphic; reconsider S9 = S as closure System of BoolePoset X by A1; take X; reconsider c = closure_op S9 as closure Function of BoolePoset X,BoolePoset X; take c; thus c is directed-sups-preserving by A2; Image c = the RelStr of S by WAYBEL10:18; then S,Image c are_isomorphic by Th26; hence thesis by A3,WAYBEL_1:7; end; Lm3: for L be LATTICE holds (ex X be set, S be full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )) implies ex X be set, c be closure Function of BoolePoset X,BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic proof let L be LATTICE; given X be set, S be full SubRelStr of BoolePoset X such that A1: S is infs-inheriting and A2: S is directed-sups-inheriting and A3: L,S are_isomorphic; reconsider S9 = S as closure System of BoolePoset X by A1; take X; reconsider c = closure_op S9 as closure Function of BoolePoset X,BoolePoset X; take c; thus c is directed-sups-preserving by A2; Image c = the RelStr of S by WAYBEL10:18; then S,Image c are_isomorphic by Th26; hence thesis by A3,WAYBEL_1:7; end; Lm4: for L1,L2 be up-complete non empty Poset for f be Function of L1,L2 st f is isomorphic for x,y be Element of L1 holds x << y implies f.x << f.y proof let L1,L2 be up-complete non empty Poset; let f be Function of L1,L2; assume A1: f is isomorphic; then reconsider g = f" as Function of L2,L1 by WAYBEL_0:67; let x,y be Element of L1; A2: g is isomorphic by A1,WAYBEL_0:68; assume A3: x << y; now let X be non empty directed Subset of L2; y in the carrier of L1; then A4: y in dom f by FUNCT_2:def 1; X c= the carrier of L2; then A5: X c= rng f by A1,WAYBEL_0:66; now let Y1 be finite Subset of g.:X; A6: f"(f.:Y1) c= Y1 by A1,FUNCT_1:82; now let v be object; assume v in f.:Y1; then ex u be object st u in dom f & u in Y1 & v = f.u by FUNCT_1:def 6; then v in f.:(g.:X) by FUNCT_1:def 6; then v in f.:(f"X) by A1,FUNCT_1:85; hence v in X by A5,FUNCT_1:77; end; then reconsider X1 = f.:Y1 as finite Subset of X by TARSKI:def 3; consider y1 be Element of L2 such that A7: y1 in X and A8: y1 is_>=_than X1 by WAYBEL_0:1; take gy1 = g.y1; y1 in the carrier of L2; then y1 in dom g by FUNCT_2:def 1; hence gy1 in g.:X by A7,FUNCT_1:def 6; Y1 c= the carrier of L1 by XBOOLE_1:1; then Y1 c= dom f by FUNCT_2:def 1; then A9: Y1 c= f"(f.:Y1) by FUNCT_1:76; g.:X1 = f"(f.:Y1) by A1,FUNCT_1:85 .= Y1 by A9,A6,XBOOLE_0:def 10; hence gy1 is_>=_than Y1 by A2,A8,Th19; end; then reconsider Y = g.:X as non empty directed Subset of L1 by WAYBEL_0:1; A10: ex_sup_of X,L2 & g preserves_sup_of X by A2,WAYBEL_0:75,def 33; assume f.y <= sup X; then g.(f.y) <= g.(sup X) by A2,WAYBEL_0:66; then y <= g.(sup X) by A1,A4,FUNCT_1:34; then y <= sup Y by A10,WAYBEL_0:def 31; then consider c be Element of L1 such that A11: c in Y and A12: x <= c by A3,WAYBEL_3:def 1; take fc = f.c; c in the carrier of L1; then c in dom f by FUNCT_2:def 1; then f.c in f.:Y by A11,FUNCT_1:def 6; then f.c in f.:(f"X) by A1,FUNCT_1:85; hence fc in X by A5,FUNCT_1:77; thus f.x <= fc by A1,A12,WAYBEL_0:66; end; hence thesis by WAYBEL_3:def 1; end; theorem Th27: for L1,L2 be up-complete non empty Poset for f be Function of L1,L2 st f is isomorphic for x,y be Element of L1 holds x << y iff f.x << f.y proof let L1,L2 be up-complete non empty Poset; let f be Function of L1,L2; assume A1: f is isomorphic; then reconsider g = f" as Function of L2,L1 by WAYBEL_0:67; let x,y be Element of L1; thus x << y implies f.x << f.y by A1,Lm4; thus f.x << f.y implies x << y proof y in the carrier of L1; then A2: y in dom f by FUNCT_2:def 1; x in the carrier of L1; then A3: x in dom f by FUNCT_2:def 1; assume f.x << f.y; then g.(f.x) << g.(f.y) by A1,Lm4,WAYBEL_0:68; then x << g.(f.y) by A1,A3,FUNCT_1:34; hence thesis by A1,A2,FUNCT_1:34; end; end; theorem Th28: for L1,L2 be up-complete non empty Poset for f be Function of L1,L2 st f is isomorphic for x be Element of L1 holds x is compact iff f.x is compact proof let L1,L2 be up-complete non empty Poset; let f be Function of L1,L2; assume A1: f is isomorphic; let x be Element of L1; thus x is compact implies f.x is compact proof assume x is compact; then x << x by WAYBEL_3:def 2; then f.x << f.x by A1,Th27; hence thesis by WAYBEL_3:def 2; end; thus f.x is compact implies x is compact proof assume f.x is compact; then f.x << f.x by WAYBEL_3:def 2; then x << x by A1,Th27; hence thesis by WAYBEL_3:def 2; end; end; theorem Th29: for L1,L2 be up-complete non empty Poset for f be Function of L1,L2 st f is isomorphic for x be Element of L1 holds f.:(compactbelow x) = compactbelow f.x proof let L1,L2 be up-complete non empty Poset; let f be Function of L1,L2; assume A1: f is isomorphic; then reconsider g = f" as Function of L2,L1 by WAYBEL_0:67; let x be Element of L1; A2: g is isomorphic by A1,WAYBEL_0:68; A3: compactbelow f.x c= f.:(compactbelow x) proof let z be object; x in the carrier of L1; then A4: x in dom f by FUNCT_2:def 1; assume z in compactbelow f.x; then z in { y where y is Element of L2: f.x >= y & y is compact } by WAYBEL_8:def 2; then consider z1 be Element of L2 such that A5: z1 = z and A6: f.x >= z1 and A7: z1 is compact; A8: g.z1 is compact by A2,A7,Th28; g.z1 <= g.(f.x) by A2,A6,WAYBEL_0:66; then g.z1 <= x by A1,A4,FUNCT_1:34; then A9: g.z1 in compactbelow x by A8,WAYBEL_8:4; z1 in the carrier of L2; then A10: z1 in rng f by A1,WAYBEL_0:66; g.z1 in the carrier of L1; then g.z1 in dom f by FUNCT_2:def 1; then f.(g.z1) in f.:(compactbelow x) by A9,FUNCT_1:def 6; hence thesis by A1,A5,A10,FUNCT_1:35; end; f.:(compactbelow x) c= compactbelow f.x proof let z be object; assume z in f.:(compactbelow x); then consider u be object such that u in dom f and A11: u in compactbelow x and A12: z = f.u by FUNCT_1:def 6; u in { y where y is Element of L1: x >= y & y is compact } by A11, WAYBEL_8:def 2; then consider u1 be Element of L1 such that A13: u1 = u and A14: x >= u1 & u1 is compact; f.u1 <= f.x & f.u1 is compact by A1,A14,Th28,WAYBEL_0:66; hence thesis by A12,A13,WAYBEL_8:4; end; hence thesis by A3,XBOOLE_0:def 10; end; theorem Th30: for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is up-complete holds L2 is up-complete proof let L1,L2 be non empty Poset; assume that A1: L1,L2 are_isomorphic and A2: L1 is up-complete; consider f be Function of L1,L2 such that A3: f is isomorphic by A1,WAYBEL_1:def 8; reconsider g = f" as Function of L2,L1 by A3,WAYBEL_0:67; A4: g is isomorphic by A3,WAYBEL_0:68; now let Y be non empty directed Subset of L2; Y c= the carrier of L2; then A5: Y c= rng f by A3,WAYBEL_0:66; now let X1 be finite Subset of g.:Y; A6: f"(f.:X1) c= X1 by A3,FUNCT_1:82; now let v be object; assume v in f.:X1; then ex u be object st u in dom f & u in X1 & v = f.u by FUNCT_1:def 6; then v in f.:(g.:Y) by FUNCT_1:def 6; then v in f.:(f"Y) by A3,FUNCT_1:85; hence v in Y by A5,FUNCT_1:77; end; then reconsider Y1 = f.:X1 as finite Subset of Y by TARSKI:def 3; consider y1 be Element of L2 such that A7: y1 in Y and A8: y1 is_>=_than Y1 by WAYBEL_0:1; take gy1 = g.y1; y1 in the carrier of L2; then y1 in dom g by FUNCT_2:def 1; hence gy1 in g.:Y by A7,FUNCT_1:def 6; X1 c= the carrier of L1 by XBOOLE_1:1; then X1 c= dom f by FUNCT_2:def 1; then A9: X1 c= f"(f.:X1) by FUNCT_1:76; g.:Y1 = f"(f.:X1) by A3,FUNCT_1:85 .= X1 by A9,A6,XBOOLE_0:def 10; hence gy1 is_>=_than X1 by A4,A8,Th19; end; then reconsider X = g.:Y as non empty directed Subset of L1 by WAYBEL_0:1; ex_sup_of X,L1 by A2,WAYBEL_0:75; then consider x be Element of L1 such that A10: X is_<=_than x and A11: for b be Element of L1 st X is_<=_than b holds x <= b by YELLOW_0:15; A12: now let y be Element of L2; assume Y is_<=_than y; then X is_<=_than g.y by A4,Th19; then x <= g.y by A11; then A13: f.x <= f.(g.y) by A3,WAYBEL_0:66; y in the carrier of L2; then y in dom g by FUNCT_2:def 1; then y in rng f by A3,FUNCT_1:33; hence f.x <= y by A3,A13,FUNCT_1:35; end; f.:X = f.:(f"Y) by A3,FUNCT_1:85 .= Y by A5,FUNCT_1:77; then Y is_<=_than f.x by A3,A10,Th19; hence ex_sup_of Y,L2 by A12,YELLOW_0:15; end; hence thesis by WAYBEL_0:75; end; theorem Th31: for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is complete satisfying_axiom_K holds L2 is satisfying_axiom_K proof let L1,L2 be non empty Poset; assume that A1: L1,L2 are_isomorphic and A2: L1 is complete satisfying_axiom_K; consider f be Function of L1,L2 such that A3: f is isomorphic by A1,WAYBEL_1:def 8; reconsider g = f" as Function of L2,L1 by A3,WAYBEL_0:67; now let x be Element of L2; A4: f preserves_sup_of compactbelow g.x & ex_sup_of compactbelow g.x,L1 by A2 ,A3,WAYBEL_0:def 33,YELLOW_0:17; A5: L2 is up-complete non empty Poset by A1,A2,Th30; x in the carrier of L2; then x in dom g by FUNCT_2:def 1; then A6: x in rng f by A3,FUNCT_1:33; hence x = f.(g.x) by A3,FUNCT_1:35 .= f.(sup compactbelow g.x) by A2,WAYBEL_8:def 3 .= sup (f.:(compactbelow g.x)) by A4,WAYBEL_0:def 31 .= sup compactbelow f.(g.x) by A2,A3,A5,Th29 .= sup compactbelow x by A3,A6,FUNCT_1:35; end; hence thesis by WAYBEL_8:def 3; end; theorem Th32: for L1,L2 be sup-Semilattice st L1,L2 are_isomorphic & L1 is lower-bounded algebraic holds L2 is algebraic proof let L1,L2 be sup-Semilattice; assume that A1: L1,L2 are_isomorphic and A2: L1 is lower-bounded algebraic; consider f be Function of L1,L2 such that A3: f is isomorphic by A1,WAYBEL_1:def 8; reconsider g = f" as Function of L2,L1 by A3,WAYBEL_0:67; A4: g is isomorphic by A3,WAYBEL_0:68; A5: now let y be Element of L2; y in the carrier of L2; then y in dom g by FUNCT_2:def 1; then A6: y in rng f by A3,FUNCT_1:33; A7: L2 is up-complete non empty Poset by A1,A2,Th30; A8: compactbelow (g.y) is non empty directed by A2,WAYBEL_8:def 4; now let Y be finite Subset of compactbelow f.(g.y); Y c= the carrier of L2 by XBOOLE_1:1; then A9: Y c= rng f by A3,WAYBEL_0:66; now let z be object; assume z in g.:Y; then consider v be object such that A10: v in dom g and A11: v in Y and A12: z = g.v by FUNCT_1:def 6; reconsider v as Element of L2 by A10; v in compactbelow f.(g.y) by A11; then v in compactbelow y by A3,A6,FUNCT_1:35; then v <= y by WAYBEL_8:4; then A13: g.v <= g.y by A4,WAYBEL_0:66; v is compact by A11,WAYBEL_8:4; then g.v is compact by A2,A4,A7,Th28; hence z in compactbelow (g.y) by A12,A13,WAYBEL_8:4; end; then reconsider X = g.:Y as finite Subset of compactbelow (g.y) by TARSKI:def 3; consider x be Element of L1 such that A14: x in compactbelow (g.y) and A15: x is_>=_than X by A8,WAYBEL_0:1; take fx = f.x; x <= g.y by A14,WAYBEL_8:4; then A16: f.x <= f.(g.y) by A3,WAYBEL_0:66; x is compact by A14,WAYBEL_8:4; then f.x is compact by A2,A3,A7,Th28; hence fx in compactbelow f.(g.y) by A16,WAYBEL_8:4; f.:X = f.:(f"Y) by A3,FUNCT_1:85 .= Y by A9,FUNCT_1:77; hence fx is_>=_than Y by A3,A15,Th19; end; then compactbelow f.(g.y) is non empty directed by WAYBEL_0:1; hence compactbelow y is non empty directed by A3,A6,FUNCT_1:35; end; L2 is up-complete & L2 is satisfying_axiom_K by A1,A2,Th30,Th31; hence thesis by A5,WAYBEL_8:def 4; end; Lm5: for L be LATTICE holds (ex X be set, c be closure Function of BoolePoset X,BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic) implies L is algebraic proof let L be LATTICE; given X be set, c be closure Function of BoolePoset X,BoolePoset X such that A1: c is directed-sups-preserving and A2: L,Image c are_isomorphic; Image c is complete LATTICE & Image c is algebraic LATTICE by A1,WAYBEL_8:24 ,YELLOW_2:35; hence thesis by A2,Th32,WAYBEL_1:6; end; theorem for L be continuous lower-bounded sup-Semilattice holds SupMap L is infs-preserving sups-preserving by WAYBEL_1:12,57,WAYBEL_5:3; :: THEOREM 4.15. (1) iff (2) theorem for L be lower-bounded LATTICE holds ( L is algebraic implies ex X be non empty set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) & (( ex X be set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) proof let L be lower-bounded LATTICE; thus L is algebraic implies ex X be non empty set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic by Lm1; thus (ex X be set, S be full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )) implies L is algebraic proof assume ex X be set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic; then ex X be set, c be closure Function of BoolePoset X,BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic by Lm3; hence thesis by Lm5; end; end; :: THEOREM 4.15. (1) iff (3) theorem for L be lower-bounded LATTICE holds ( L is algebraic implies ex X be non empty set, c be closure Function of BoolePoset X,BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic ) & (( ex X be set, c be closure Function of BoolePoset X,BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic ) implies L is algebraic ) proof let L be lower-bounded LATTICE; hereby assume L is algebraic; then ex X be non empty set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic by Lm1; hence ex X be non empty set, c be closure Function of BoolePoset X, BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic by Lm2; end; thus thesis by Lm5; end;