### The Mizar article:

### Bases of Continuous Lattices

**by****Robert Milewski**

- Received November 28, 1998
Copyright (c) 1998 Association of Mizar Users

- MML identifier: WAYBEL23
- [ MML identifier index ]

environ vocabulary ORDERS_1, WAYBEL_8, WAYBEL_3, BOOLE, WAYBEL_0, COMPTS_1, RELAT_2, YELLOW_1, TARSKI, FILTER_2, YELLOW_0, ORDINAL2, LATTICE3, LATTICES, FINSET_1, CAT_1, BHSP_3, QUANTAL1, FILTER_0, PRE_TOPC, CARD_1, SETFAM_1, ORDINAL1, SUBSET_1, REALSET1, FUNCT_1, WELLORD2, RELAT_1, SEQM_3, YELLOW_2, WAYBEL_1, WELLORD1, SGRAPH1, WAYBEL23, RLVECT_3; notation TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, REALSET1, FUNCT_1, STRUCT_0, FUNCT_2, FINSET_1, ORDINAL1, ORDINAL2, CARD_1, PRE_TOPC, ORDERS_1, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_8; constructors TOPS_2, CANTOR_1, LATTICE3, ORDERS_3, YELLOW_3, WAYBEL_1, WAYBEL_3, WAYBEL_8; clusters STRUCT_0, FINSET_1, CARD_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_3, WAYBEL_7, WAYBEL_8, WAYBEL14, RELSET_1, SUBSET_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, LATTICE3, YELLOW_0, XBOOLE_0; theorems TARSKI, SETFAM_1, ZFMISC_1, FUNCT_1, FUNCT_2, FINSET_1, PRE_TOPC, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_5, YELLOW12, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_7, WAYBEL_8, WAYBEL10, WAYBEL13, WAYBEL20, WAYBEL21, RELSET_1, XBOOLE_0, XBOOLE_1; schemes ORDINAL1, FUNCT_2, MONOID_1, YELLOW_2; begin :: Preliminaries theorem Th1: for L be non empty Poset for x be Element of L holds compactbelow x = waybelow x /\ the carrier of CompactSublatt L proof let L be non empty Poset; let x be Element of L; A1: compactbelow x c= waybelow x /\ the carrier of CompactSublatt L proof let y be set; assume y in compactbelow x; then y in downarrow x /\ the carrier of CompactSublatt L by WAYBEL_8:5; then A2: y in downarrow x & y in the carrier of CompactSublatt L by XBOOLE_0:def 3; then reconsider y1 = y as Element of L; A3: y1 <= x by A2,WAYBEL_0:17; y1 is compact by A2,WAYBEL_8:def 1; then y1 << y1 by WAYBEL_3:def 2; then y1 << x by A3,WAYBEL_3:2; then y1 in waybelow x by WAYBEL_3:7; hence y in waybelow x /\ the carrier of CompactSublatt L by A2,XBOOLE_0:def 3; end; waybelow x /\ the carrier of CompactSublatt L c= compactbelow x proof let y be set; assume y in waybelow x /\ the carrier of CompactSublatt L; then A4: y in waybelow x & y in the carrier of CompactSublatt L by XBOOLE_0:def 3; then reconsider y1 = y as Element of L; y1 << x by A4,WAYBEL_3:7; then y1 <= x by WAYBEL_3:1; then y in downarrow x by WAYBEL_0:17; then y in downarrow x /\ the carrier of CompactSublatt L by A4,XBOOLE_0:def 3; hence y in compactbelow x by WAYBEL_8:5; end; hence compactbelow x = waybelow x /\ the carrier of CompactSublatt L by A1,XBOOLE_0:def 10 ; end; definition let L be non empty reflexive transitive RelStr; let X be Subset of InclPoset Ids L; redefine func union X -> Subset of L; coherence proof union X c= the carrier of L proof let x be set; assume x in union X; then consider Y be set such that A1: x in Y and A2: Y in X by TARSKI:def 4; Y is Element of InclPoset Ids L by A2; then reconsider Y as Ideal of L by YELLOW_2:43; x in Y by A1; hence x in the carrier of L; end; hence union X is Subset of L; end; end; Lm1: for X be non empty set for Y be Subset of InclPoset X st ex_sup_of Y,InclPoset X holds union Y c= sup Y proof let X be non empty set; let Y be Subset of InclPoset X; assume A1: ex_sup_of Y,InclPoset X; now let x be set; assume A2: x in Y; then reconsider x1 = x as Element of InclPoset X; sup Y is_>=_than Y by A1,YELLOW_0:30; then sup Y >= x1 by A2,LATTICE3:def 9; hence x c= sup Y by YELLOW_1:3; end; hence union Y c= sup Y by ZFMISC_1:94; end; theorem Th2: for L be non empty RelStr for X,Y be Subset of L st X c= Y holds finsups X c= finsups Y proof let L be non empty RelStr; let X,Y be Subset of L; assume A1: X c= Y; let x be set; assume x in finsups X; then x in {"\/"(V,L) where V is finite Subset of X: ex_sup_of V,L} by WAYBEL_0:def 27; then consider Z be finite Subset of X such that A2: x = "\/"(Z,L) and A3: ex_sup_of Z,L; reconsider Z as finite Subset of Y by A1,XBOOLE_1:1; ex_sup_of Z,L by A3; then x in {"\/"(V,L) where V is finite Subset of Y: ex_sup_of V,L} by A2; hence x in finsups Y by WAYBEL_0:def 27; end; theorem Th3: for L be non empty transitive RelStr for S be sups-inheriting non empty full SubRelStr of L for X be Subset of L for Y be Subset of S st X = Y holds finsups X c= finsups Y proof let L be non empty transitive RelStr; let S be sups-inheriting non empty full SubRelStr of L; let X be Subset of L; let Y be Subset of S; assume A1: X = Y; let x be set; assume x in finsups X; then x in {"\/"(V,L) where V is finite Subset of X: ex_sup_of V,L} by WAYBEL_0:def 27; then consider Z be finite Subset of X such that A2: x = "\/"(Z,L) and A3: ex_sup_of Z,L; reconsider Z as finite Subset of Y by A1; Z c= the carrier of S by XBOOLE_1:1; then reconsider Z1 = Z as Subset of S; "\/"(Z1,L) in the carrier of S by A3,YELLOW_0:def 19; then ex_sup_of Z1,S & x = "\/"(Z1,S) by A2,A3,YELLOW_0:65; then x in {"\/"(V,S) where V is finite Subset of Y: ex_sup_of V,S}; hence x in finsups Y by WAYBEL_0:def 27; end; theorem for L be complete transitive antisymmetric (non empty RelStr) for S be sups-inheriting non empty full SubRelStr of L for X be Subset of L for Y be Subset of S st X = Y holds finsups X = finsups Y proof let L be complete transitive antisymmetric (non empty RelStr); let S be sups-inheriting non empty full SubRelStr of L; let X be Subset of L; let Y be Subset of S; assume A1: X = Y; hence finsups X c= finsups Y by Th3; let x be set; assume x in finsups Y; then x in {"\/"(V,S) where V is finite Subset of Y: ex_sup_of V,S} by WAYBEL_0:def 27; then consider Z be finite Subset of Y such that A2: x = "\/"(Z,S) and ex_sup_of Z,S; reconsider Z as finite Subset of X by A1; Z c= the carrier of S by XBOOLE_1:1; then reconsider Z1 = Z as Subset of S; A3: ex_sup_of Z1,L by YELLOW_0:17; then "\/"(Z1,L) in the carrier of S by YELLOW_0:def 19; then x = "\/"(Z1,L) by A2,A3,YELLOW_0:65; then x in {"\/"(V,L) where V is finite Subset of X: ex_sup_of V,L} by A3; hence x in finsups X by WAYBEL_0:def 27; end; theorem Th5: for L be complete sup-Semilattice for S be join-inheriting non empty full SubRelStr of L st Bottom L in the carrier of S for X be Subset of L for Y be Subset of S st X = Y holds finsups Y c= finsups X proof let L be complete sup-Semilattice; let S be join-inheriting non empty full SubRelStr of L; assume A1: Bottom L in the carrier of S; let X be Subset of L; let Y be Subset of S; assume A2: X = Y; let x be set; assume x in finsups Y; then x in {"\/"(V,S) where V is finite Subset of Y: ex_sup_of V,S} by WAYBEL_0:def 27; then consider Z be finite Subset of Y such that A3: x = "\/"(Z,S) and A4: ex_sup_of Z,S; reconsider Z as finite Subset of X by A2; now per cases; suppose A5: Z is non empty; Z c= the carrier of S by XBOOLE_1:1; then reconsider Z1 = Z as finite non empty Subset of S by A5; A6: ex_sup_of Z1,L by YELLOW_0:17; "\/"(Z1,L) in the carrier of S by WAYBEL21:15; then reconsider xl = "\/"(Z1,L) as Element of S; A7: "\/"(Z1, L) is_>=_than Z1 & for b be Element of L st b is_>=_than Z1 holds "\/"(Z1, L) <= b by A6,YELLOW_0:30; A8: xl is_>=_than Z1 proof let b be Element of S; reconsider b1 = b as Element of L by YELLOW_0:59; assume b in Z1; then b1 <= "\/"(Z1, L) by A7,LATTICE3:def 9; hence b <= xl by YELLOW_0:61; end; now let b be Element of S; reconsider b1 = b as Element of L by YELLOW_0:59; assume A9: b is_>=_than Z1; b1 is_>=_than Z1 proof let c1 be Element of L; assume A10: c1 in Z1; then reconsider c = c1 as Element of S; c <= b by A9,A10,LATTICE3:def 9; hence c1 <= b1 by YELLOW_0:60; end; then "\/"(Z1, L) <= b1 by A6,YELLOW_0:30; hence xl <= b by YELLOW_0:61; end; then "\/"(Z1,S) = "\/"(Z1,L) by A8,YELLOW_0:30; then x in { "\/"(V,L) where V is finite Subset of X: ex_sup_of V,L } by A3,A6; hence x in finsups X by WAYBEL_0:def 27; suppose A11: Z is empty; then A12: x = Bottom S by A3,YELLOW_0:def 11; reconsider dS = Bottom S as Element of L by YELLOW_0:59; reconsider dL = Bottom L as Element of S by A1; A13: dL = "\/"({},L) by YELLOW_0:def 11; S is lower-bounded by A4,A11,WAYBEL20:6; then Bottom S <= dL by YELLOW_0:44; then A14: dS <= Bottom L by YELLOW_0:60; Bottom L <= dS by YELLOW_0:44; then A15: dS = Bottom L by A14,YELLOW_0:def 3; ex_sup_of Z,L by YELLOW_0:17; then x in { "\/"(V,L) where V is finite Subset of X: ex_sup_of V,L } by A11,A12,A13,A15; hence x in finsups X by WAYBEL_0:def 27; end; hence x in finsups X; end; theorem Th6: for L be lower-bounded sup-Semilattice for X be Subset of InclPoset Ids L holds sup X = downarrow finsups union X proof let L be lower-bounded sup-Semilattice; let X be Subset of InclPoset Ids L; A1: union X c= downarrow finsups union X & for I be Ideal of L st union X c= I holds downarrow finsups union X c= I by WAYBEL_0:61; ex_sup_of X,InclPoset Ids L by YELLOW_0:17; then A2: union X c= sup X by Lm1; reconsider a = downarrow finsups union X as Element of InclPoset Ids L by YELLOW_2:43; now let b be Element of InclPoset Ids L; assume b in X; then b c= union X by ZFMISC_1:92; then b c= downarrow finsups union X by A1,XBOOLE_1:1; hence b <= a by YELLOW_1:3; end; then A3: a is_>=_than X by LATTICE3:def 9; now let b be Element of InclPoset Ids L; reconsider b1 = b as Ideal of L by YELLOW_2:43; assume b is_>=_than X; then b >= sup X by YELLOW_0:32; then sup X c= b1 by YELLOW_1:3; then union X c= b1 by A2,XBOOLE_1:1; then downarrow finsups union X c= b1 by WAYBEL_0:61; hence a <= b by YELLOW_1:3; end; hence thesis by A3,YELLOW_0:32; end; theorem Th7: for L be reflexive transitive RelStr for X be Subset of L holds downarrow downarrow X = downarrow X proof let L be reflexive transitive RelStr; let X be Subset of L; A1: downarrow X c= downarrow downarrow X by WAYBEL_0:16; downarrow downarrow X c= downarrow X proof let x be set; assume A2: x in downarrow downarrow X; then reconsider x1 = x as Element of L; consider y be Element of L such that A3: y >= x1 and A4: y in downarrow X by A2,WAYBEL_0:def 15; consider z be Element of L such that A5: z >= y and A6: z in X by A4,WAYBEL_0:def 15; z >= x1 by A3,A5,YELLOW_0:def 2; hence x in downarrow X by A6,WAYBEL_0:def 15; end; hence downarrow downarrow X = downarrow X by A1,XBOOLE_0:def 10; end; theorem for L be reflexive transitive RelStr for X be Subset of L holds uparrow uparrow X = uparrow X proof let L be reflexive transitive RelStr; let X be Subset of L; A1: uparrow X c= uparrow uparrow X by WAYBEL_0:16; uparrow uparrow X c= uparrow X proof let x be set; assume A2: x in uparrow uparrow X; then reconsider x1 = x as Element of L; consider y be Element of L such that A3: y <= x1 and A4: y in uparrow X by A2,WAYBEL_0:def 16; consider z be Element of L such that A5: z <= y and A6: z in X by A4,WAYBEL_0:def 16; z <= x1 by A3,A5,YELLOW_0:def 2; hence x in uparrow X by A6,WAYBEL_0:def 16; end; hence uparrow uparrow X = uparrow X by A1,XBOOLE_0:def 10; end; theorem for L be non empty reflexive transitive RelStr for x be Element of L holds downarrow downarrow x = downarrow x proof let L be non empty reflexive transitive RelStr; let x be Element of L; A1: downarrow x c= downarrow downarrow x by WAYBEL_0:16; downarrow downarrow x c= downarrow x proof let v be set; assume A2: v in downarrow downarrow x; then reconsider v1 = v as Element of L; consider y be Element of L such that A3: y >= v1 and A4: y in downarrow x by A2,WAYBEL_0:def 15; x >= y by A4,WAYBEL_0:17; then x >= v1 by A3,YELLOW_0:def 2; hence v in downarrow x by WAYBEL_0:17; end; hence downarrow downarrow x = downarrow x by A1,XBOOLE_0:def 10; end; theorem for L be non empty reflexive transitive RelStr for x be Element of L holds uparrow uparrow x = uparrow x proof let L be non empty reflexive transitive RelStr; let x be Element of L; A1: uparrow x c= uparrow uparrow x by WAYBEL_0:16; uparrow uparrow x c= uparrow x proof let v be set; assume A2: v in uparrow uparrow x; then reconsider v1 = v as Element of L; consider y be Element of L such that A3: y <= v1 and A4: y in uparrow x by A2,WAYBEL_0:def 16; x <= y by A4,WAYBEL_0:18; then x <= v1 by A3,YELLOW_0:def 2; hence v in uparrow x by WAYBEL_0:18; end; hence uparrow uparrow x = uparrow x by A1,XBOOLE_0:def 10; end; theorem Th11: for L be non empty RelStr for S be non empty SubRelStr of L for X be Subset of L for Y be Subset of S st X = Y holds downarrow Y c= downarrow X proof let L be non empty RelStr; let S be non empty SubRelStr of L; let X be Subset of L; let Y be Subset of S; assume A1: X = Y; let x be set; assume A2: x in downarrow Y; then reconsider x1 = x as Element of S; consider y1 be Element of S such that A3: y1 >= x1 and A4: y1 in Y by A2,WAYBEL_0:def 15; reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0:59; y2 >= x2 by A3,YELLOW_0:60; hence x in downarrow X by A1,A4,WAYBEL_0:def 15; end; theorem Th12: for L be non empty RelStr for S be non empty SubRelStr of L for X be Subset of L for Y be Subset of S st X = Y holds uparrow Y c= uparrow X proof let L be non empty RelStr; let S be non empty SubRelStr of L; let X be Subset of L; let Y be Subset of S; assume A1: X = Y; let x be set; assume A2: x in uparrow Y; then reconsider x1 = x as Element of S; consider y1 be Element of S such that A3: y1 <= x1 and A4: y1 in Y by A2,WAYBEL_0:def 16; reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0:59; y2 <= x2 by A3,YELLOW_0:60; hence x in uparrow X by A1,A4,WAYBEL_0:def 16; end; theorem for L be non empty RelStr for S be non empty SubRelStr of L for x be Element of L for y be Element of S st x = y holds downarrow y c= downarrow x proof let L be non empty RelStr; let S be non empty SubRelStr of L; let x be Element of L; let y be Element of S; assume A1: x = y; downarrow x = downarrow {x} & downarrow y = downarrow {y} by WAYBEL_0:def 17; hence thesis by A1,Th11; end; theorem for L be non empty RelStr for S be non empty SubRelStr of L for x be Element of L for y be Element of S st x = y holds uparrow y c= uparrow x proof let L be non empty RelStr; let S be non empty SubRelStr of L; let x be Element of L; let y be Element of S; assume A1: x = y; uparrow x = uparrow {x} & uparrow y = uparrow {y} by WAYBEL_0:def 18; hence thesis by A1,Th12; end; begin :: Relational Subsets definition let L be non empty RelStr; let S be Subset of L; attr S is meet-closed means :Def1: subrelstr S is meet-inheriting; end; definition let L be non empty RelStr; let S be Subset of L; attr S is join-closed means :Def2: subrelstr S is join-inheriting; end; definition let L be non empty RelStr; let S be Subset of L; attr S is infs-closed means :Def3: subrelstr S is infs-inheriting; end; definition let L be non empty RelStr; let S be Subset of L; attr S is sups-closed means :Def4: subrelstr S is sups-inheriting; end; definition let L be non empty RelStr; cluster infs-closed -> meet-closed Subset of L; coherence proof let S be Subset of L; assume S is infs-closed; then reconsider S1 = subrelstr S as infs-inheriting SubRelStr of L by Def3; S1 is meet-inheriting; hence S is meet-closed by Def1; end; cluster sups-closed -> join-closed Subset of L; coherence proof let S be Subset of L; assume S is sups-closed; then reconsider S1 = subrelstr S as sups-inheriting SubRelStr of L by Def4; S1 is join-inheriting; hence S is join-closed by Def2; end; end; definition let L be non empty RelStr; cluster infs-closed sups-closed non empty Subset of L; existence proof the carrier of L c= the carrier of L; then reconsider S = the carrier of L as Subset of L; take S; thus subrelstr S is infs-inheriting proof the carrier of subrelstr S = S by YELLOW_0:def 15; then for X be Subset of subrelstr S st ex_inf_of X,L holds "/\"(X,L) in the carrier of subrelstr S; hence thesis by YELLOW_0:def 18; end; thus subrelstr S is sups-inheriting proof the carrier of subrelstr S = S by YELLOW_0:def 15; then for X be Subset of subrelstr S st ex_sup_of X,L holds "\/"(X,L) in the carrier of subrelstr S; hence thesis by YELLOW_0:def 19; end; thus thesis; end; end; theorem Th15: for L be non empty RelStr for S be Subset of L holds S is meet-closed iff for x,y be Element of L st x in S & y in S & ex_inf_of {x,y},L holds inf {x,y} in S proof let L be non empty RelStr; let S be Subset of L; thus S is meet-closed implies for x,y be Element of L st x in S & y in S & ex_inf_of {x,y},L holds inf {x,y} in S proof assume S is meet-closed; then A1: subrelstr S is meet-inheriting by Def1; let x,y be Element of L; assume that A2: x in S and A3: y in S and A4: ex_inf_of {x,y},L; the carrier of subrelstr S = S by YELLOW_0:def 15; hence inf {x,y} in S by A1,A2,A3,A4,YELLOW_0:def 16; end; assume A5: for x,y be Element of L st x in S & y in S & ex_inf_of {x,y},L holds inf {x,y} in S; now let x,y be Element of L; assume that A6: x in the carrier of subrelstr S and A7: y in the carrier of subrelstr S and A8: ex_inf_of {x,y},L; the carrier of subrelstr S = S by YELLOW_0:def 15; hence inf {x,y} in the carrier of subrelstr S by A5,A6,A7,A8; end; then subrelstr S is meet-inheriting by YELLOW_0:def 16; hence S is meet-closed by Def1; end; theorem Th16: for L be non empty RelStr for S be Subset of L holds S is join-closed iff for x,y be Element of L st x in S & y in S & ex_sup_of {x,y},L holds sup {x,y} in S proof let L be non empty RelStr; let S be Subset of L; thus S is join-closed implies for x,y be Element of L st x in S & y in S & ex_sup_of {x,y},L holds sup {x,y} in S proof assume S is join-closed; then A1: subrelstr S is join-inheriting by Def2; let x,y be Element of L; assume that A2: x in S and A3: y in S and A4: ex_sup_of {x,y},L; the carrier of subrelstr S = S by YELLOW_0:def 15; hence sup {x,y} in S by A1,A2,A3,A4,YELLOW_0:def 17; end; assume A5: for x,y be Element of L st x in S & y in S & ex_sup_of {x,y},L holds sup {x,y} in S; now let x,y be Element of L; assume that A6: x in the carrier of subrelstr S and A7: y in the carrier of subrelstr S and A8: ex_sup_of {x,y},L; the carrier of subrelstr S = S by YELLOW_0:def 15; hence sup {x,y} in the carrier of subrelstr S by A5,A6,A7,A8; end; then subrelstr S is join-inheriting by YELLOW_0:def 17; hence S is join-closed by Def2; end; theorem for L be antisymmetric with_infima RelStr for S be Subset of L holds S is meet-closed iff for x,y be Element of L st x in S & y in S holds inf {x,y} in S proof let L be antisymmetric with_infima RelStr; let S be Subset of L; thus S is meet-closed implies for x,y be Element of L st x in S & y in S holds inf {x,y} in S proof assume A1: S is meet-closed; let x,y be Element of L such that A2: x in S and A3: y in S; ex_inf_of {x,y},L by YELLOW_0:21; hence inf {x,y} in S by A1,A2,A3,Th15; end; assume for x,y be Element of L st x in S & y in S holds inf {x,y} in S; then for x,y be Element of L st x in S & y in S & ex_inf_of {x,y},L holds inf {x,y} in S; hence S is meet-closed by Th15; end; theorem Th18: for L be antisymmetric with_suprema RelStr for S be Subset of L holds S is join-closed iff for x,y be Element of L st x in S & y in S holds sup {x,y} in S proof let L be antisymmetric with_suprema RelStr; let S be Subset of L; thus S is join-closed implies for x,y be Element of L st x in S & y in S holds sup {x,y} in S proof assume A1: S is join-closed; let x,y be Element of L such that A2: x in S and A3: y in S; ex_sup_of {x,y},L by YELLOW_0:20; hence sup {x,y} in S by A1,A2,A3,Th16; end; assume for x,y be Element of L st x in S & y in S holds sup {x,y} in S; then for x,y be Element of L st x in S & y in S & ex_sup_of {x,y},L holds sup {x,y} in S; hence S is join-closed by Th16; end; theorem for L be non empty RelStr for S be Subset of L holds S is infs-closed iff for X be Subset of S st ex_inf_of X,L holds "/\"(X,L) in S proof let L be non empty RelStr; let S be Subset of L; thus S is infs-closed implies for X be Subset of S st ex_inf_of X,L holds "/\"(X,L) in S proof assume S is infs-closed; then A1: subrelstr S is infs-inheriting by Def3; let X be Subset of S; X is Subset of subrelstr S by YELLOW_0:def 15; then A2: X is Subset of subrelstr S; assume ex_inf_of X,L; then "/\"(X,L) in the carrier of subrelstr S by A1,A2,YELLOW_0:def 18; hence "/\"(X,L) in S by YELLOW_0:def 15; end; assume A3: for X be Subset of S st ex_inf_of X,L holds "/\"(X,L) in S; now let X be Subset of subrelstr S; A4: X is Subset of S by YELLOW_0:def 15; assume ex_inf_of X,L; then "/\"(X,L) in S by A3,A4; hence "/\"(X,L) in the carrier of subrelstr S by YELLOW_0:def 15; end; then subrelstr S is infs-inheriting by YELLOW_0:def 18; hence S is infs-closed by Def3; end; theorem for L be non empty RelStr for S be Subset of L holds S is sups-closed iff for X be Subset of S st ex_sup_of X,L holds "\/"(X,L) in S proof let L be non empty RelStr; let S be Subset of L; thus S is sups-closed implies for X be Subset of S st ex_sup_of X,L holds "\/"(X,L) in S proof assume S is sups-closed; then A1: subrelstr S is sups-inheriting by Def4; let X be Subset of S; X is Subset of subrelstr S by YELLOW_0:def 15; then A2: X is Subset of subrelstr S; assume ex_sup_of X,L; then "\/"(X,L) in the carrier of subrelstr S by A1,A2,YELLOW_0:def 19; hence "\/"(X,L) in S by YELLOW_0:def 15; end; assume A3: for X be Subset of S st ex_sup_of X,L holds "\/"(X,L) in S; now let X be Subset of subrelstr S; A4: X is Subset of S by YELLOW_0:def 15; assume ex_sup_of X,L; then "\/"(X,L) in S by A3,A4; hence "\/"(X,L) in the carrier of subrelstr S by YELLOW_0:def 15; end; then subrelstr S is sups-inheriting by YELLOW_0:def 19; hence S is sups-closed by Def4; end; theorem Th21: for L be non empty transitive RelStr for S be infs-closed non empty Subset of L for X be Subset of S st ex_inf_of X,L holds ex_inf_of X,subrelstr S & "/\"(X,subrelstr S) = "/\"(X,L) proof let L be non empty transitive RelStr; let S be infs-closed non empty Subset of L; let X be Subset of S; A1: subrelstr S is infs-inheriting non empty full SubRelStr of L by Def3; X is Subset of subrelstr S by YELLOW_0:def 15; then A2: X is Subset of subrelstr S; assume A3: ex_inf_of X,L; then "/\"(X,L) in the carrier of subrelstr S by A1,A2,YELLOW_0:def 18; hence ex_inf_of X,subrelstr S & "/\"(X,subrelstr S) = "/\"(X,L) by A2,A3,YELLOW_0:64; end; theorem Th22: for L be non empty transitive RelStr for S be sups-closed non empty Subset of L for X be Subset of S st ex_sup_of X,L holds ex_sup_of X,subrelstr S & "\/"(X,subrelstr S) = "\/"(X,L) proof let L be non empty transitive RelStr; let S be sups-closed non empty Subset of L; let X be Subset of S; A1: subrelstr S is sups-inheriting non empty full SubRelStr of L by Def4; X is Subset of subrelstr S by YELLOW_0:def 15; then A2: X is Subset of subrelstr S; assume A3: ex_sup_of X,L; then "\/"(X,L) in the carrier of subrelstr S by A1,A2,YELLOW_0:def 19; hence ex_sup_of X,subrelstr S & "\/"(X,subrelstr S) = "\/"(X,L) by A2,A3,YELLOW_0:65; end; theorem for L be non empty transitive RelStr for S be meet-closed non empty Subset of L for x,y be Element of S st ex_inf_of {x,y},L holds ex_inf_of {x,y},subrelstr S & "/\"({x,y},subrelstr S) = "/\"({x,y},L) proof let L be non empty transitive RelStr; let S be meet-closed non empty Subset of L; let x,y be Element of S; A1: subrelstr S is meet-inheriting non empty full SubRelStr of L by Def1; A2: x is Element of subrelstr S & y is Element of subrelstr S by YELLOW_0:def 15; then A3: x is Element of subrelstr S & y is Element of subrelstr S; assume A4: ex_inf_of {x,y},L; then "/\"({x,y},L) in the carrier of subrelstr S by A1,A2,YELLOW_0:def 16; hence ex_inf_of {x,y},subrelstr S & "/\"({x,y},subrelstr S) = "/\"({x,y},L ) by A3,A4,YELLOW_0:66; end; theorem for L be non empty transitive RelStr for S be join-closed non empty Subset of L for x,y be Element of S st ex_sup_of {x,y},L holds ex_sup_of {x,y},subrelstr S & "\/"({x,y},subrelstr S) = "\/"({x,y},L) proof let L be non empty transitive RelStr; let S be join-closed non empty Subset of L; let x,y be Element of S; A1: subrelstr S is join-inheriting non empty full SubRelStr of L by Def2; A2: x is Element of subrelstr S & y is Element of subrelstr S by YELLOW_0:def 15; then A3: x is Element of subrelstr S & y is Element of subrelstr S; assume A4: ex_sup_of {x,y},L; then "\/"({x,y},L) in the carrier of subrelstr S by A1,A2,YELLOW_0:def 17; hence ex_sup_of {x,y},subrelstr S & "\/"({x,y},subrelstr S) = "\/"({x,y},L ) by A3,A4,YELLOW_0:67; end; theorem Th25: for L be with_infima antisymmetric transitive RelStr for S be non empty meet-closed Subset of L holds subrelstr S is with_infima proof let L be with_infima antisymmetric transitive RelStr; let S be non empty meet-closed Subset of L; subrelstr S is non empty meet-inheriting full SubRelStr of L by Def1; hence subrelstr S is with_infima; end; theorem Th26: for L be with_suprema antisymmetric transitive RelStr for S be non empty join-closed Subset of L holds subrelstr S is with_suprema proof let L be with_suprema antisymmetric transitive RelStr; let S be non empty join-closed Subset of L; subrelstr S is non empty join-inheriting full SubRelStr of L by Def2; hence subrelstr S is with_suprema; end; definition let L be with_infima antisymmetric transitive RelStr; let S be non empty meet-closed Subset of L; cluster subrelstr S -> with_infima; coherence by Th25; end; definition let L be with_suprema antisymmetric transitive RelStr; let S be non empty join-closed Subset of L; cluster subrelstr S -> with_suprema; coherence by Th26; end; theorem for L be complete transitive antisymmetric (non empty RelStr) for S be infs-closed non empty Subset of L for X be Subset of S holds "/\"(X,subrelstr S) = "/\"(X,L) proof let L be complete transitive antisymmetric (non empty RelStr); let S be infs-closed non empty Subset of L; let X be Subset of S; ex_inf_of X,L by YELLOW_0:17; hence "/\"(X,subrelstr S) = "/\"(X,L) by Th21; end; theorem for L be complete transitive antisymmetric (non empty RelStr) for S be sups-closed non empty Subset of L for X be Subset of S holds "\/"(X,subrelstr S) = "\/"(X,L) proof let L be complete transitive antisymmetric (non empty RelStr); let S be sups-closed non empty Subset of L; let X be Subset of S; ex_sup_of X,L by YELLOW_0:17; hence "\/"(X,subrelstr S) = "\/"(X,L) by Th22; end; theorem Th29: for L be Semilattice for S be meet-closed Subset of L holds S is filtered proof let L be Semilattice; let S be meet-closed Subset of L; subrelstr S is meet-inheriting by Def1; hence S is filtered by YELLOW12:26; end; theorem Th30: for L be sup-Semilattice for S be join-closed Subset of L holds S is directed proof let L be sup-Semilattice; let S be join-closed Subset of L; subrelstr S is join-inheriting by Def2; hence S is directed by YELLOW12:27; end; definition let L be Semilattice; cluster meet-closed -> filtered Subset of L; coherence by Th29; end; definition let L be sup-Semilattice; cluster join-closed -> directed Subset of L; coherence by Th30; end; theorem for L be Semilattice for S be upper non empty Subset of L holds S is Filter of L iff S is meet-closed proof let L be Semilattice; let S be upper non empty Subset of L; S is Filter of L iff subrelstr S is meet-inheriting by WAYBEL_0:63; hence S is Filter of L iff S is meet-closed by Def1; end; theorem for L be sup-Semilattice for S be lower non empty Subset of L holds S is Ideal of L iff S is join-closed proof let L be sup-Semilattice; let S be lower non empty Subset of L; S is Ideal of L iff subrelstr S is join-inheriting by WAYBEL_0:64; hence S is Ideal of L iff S is join-closed by Def2; end; theorem Th33: for L be non empty RelStr for S1,S2 be join-closed Subset of L holds S1 /\ S2 is join-closed proof let L be non empty RelStr; let S1,S2 be join-closed Subset of L; A1: subrelstr S1 is join-inheriting & subrelstr S2 is join-inheriting by Def2; now let x,y be Element of L; assume that A2: x in the carrier of subrelstr (S1 /\ S2) and A3: y in the carrier of subrelstr (S1 /\ S2) and A4: ex_sup_of {x,y},L; x in S1 /\ S2 & y in S1 /\ S2 by A2,A3,YELLOW_0:def 15; then x in S1 & x in S2 & y in S1 & y in S2 by XBOOLE_0:def 3; then x in the carrier of subrelstr S1 & x in the carrier of subrelstr S2 & y in the carrier of subrelstr S1 & y in the carrier of subrelstr S2 by YELLOW_0:def 15; then sup {x,y} in the carrier of subrelstr S1 & sup {x,y} in the carrier of subrelstr S2 by A1,A4,YELLOW_0:def 17; then sup {x,y} in S1 & sup {x,y} in S2 by YELLOW_0:def 15; then sup {x,y} in S1 /\ S2 by XBOOLE_0:def 3; hence sup {x,y} in the carrier of subrelstr (S1 /\ S2) by YELLOW_0:def 15 ; end; then subrelstr (S1 /\ S2) is join-inheriting by YELLOW_0:def 17; hence S1 /\ S2 is join-closed by Def2; end; theorem for L be non empty RelStr for S1,S2 be meet-closed Subset of L holds S1 /\ S2 is meet-closed proof let L be non empty RelStr; let S1,S2 be meet-closed Subset of L; A1: subrelstr S1 is meet-inheriting & subrelstr S2 is meet-inheriting by Def1; now let x,y be Element of L; assume that A2: x in the carrier of subrelstr (S1 /\ S2) and A3: y in the carrier of subrelstr (S1 /\ S2) and A4: ex_inf_of {x,y},L; x in S1 /\ S2 & y in S1 /\ S2 by A2,A3,YELLOW_0:def 15; then x in S1 & x in S2 & y in S1 & y in S2 by XBOOLE_0:def 3; then x in the carrier of subrelstr S1 & x in the carrier of subrelstr S2 & y in the carrier of subrelstr S1 & y in the carrier of subrelstr S2 by YELLOW_0:def 15; then inf {x,y} in the carrier of subrelstr S1 & inf {x,y} in the carrier of subrelstr S2 by A1,A4,YELLOW_0:def 16; then inf {x,y} in S1 & inf {x,y} in S2 by YELLOW_0:def 15; then inf {x,y} in S1 /\ S2 by XBOOLE_0:def 3; hence inf {x,y} in the carrier of subrelstr (S1 /\ S2) by YELLOW_0:def 15 ; end; then subrelstr (S1 /\ S2) is meet-inheriting by YELLOW_0:def 16; hence S1 /\ S2 is meet-closed by Def1; end; theorem Th35: for L be sup-Semilattice for x be Element of L holds downarrow x is join-closed proof let L be sup-Semilattice; let x be Element of L; reconsider x1 = x as Element of L; now let y,z be Element of L; assume that A1: y in the carrier of subrelstr downarrow x and A2: z in the carrier of subrelstr downarrow x and ex_sup_of {y,z},L; y in downarrow x & z in downarrow x by A1,A2,YELLOW_0:def 15; then y <= x1 & z <= x1 by WAYBEL_0:17; then y"\/"z <= x1 by YELLOW_5:9; then y"\/"z in downarrow x by WAYBEL_0:17; then sup {y,z} in downarrow x by YELLOW_0:41; hence sup {y,z} in the carrier of subrelstr downarrow x by YELLOW_0:def 15; end; then subrelstr downarrow x is join-inheriting by YELLOW_0:def 17; hence downarrow x is join-closed by Def2; end; theorem Th36: for L be Semilattice for x be Element of L holds downarrow x is meet-closed proof let L be Semilattice; let x be Element of L; reconsider x1 = x as Element of L; now let y,z be Element of L; assume that A1: y in the carrier of subrelstr downarrow x and z in the carrier of subrelstr downarrow x and ex_inf_of {y,z},L; y in downarrow x by A1,YELLOW_0:def 15; then A2: y <= x1 by WAYBEL_0:17; y"/\"z <= y by YELLOW_0:23; then y"/\"z <= x1 by A2,YELLOW_0:def 2; then y"/\"z in downarrow x by WAYBEL_0:17; then inf {y,z} in downarrow x by YELLOW_0:40; hence inf {y,z} in the carrier of subrelstr downarrow x by YELLOW_0:def 15; end; then subrelstr downarrow x is meet-inheriting by YELLOW_0:def 16; hence downarrow x is meet-closed by Def1; end; theorem Th37: for L be sup-Semilattice for x be Element of L holds uparrow x is join-closed proof let L be sup-Semilattice; let x be Element of L; reconsider x1 = x as Element of L; now let y,z be Element of L; assume that A1: y in the carrier of subrelstr uparrow x and z in the carrier of subrelstr uparrow x and ex_sup_of {y,z},L; y in uparrow x by A1,YELLOW_0:def 15; then A2: y >= x1 by WAYBEL_0:18; y"\/"z >= y by YELLOW_0:22; then y"\/"z >= x1 by A2,YELLOW_0:def 2; then y"\/"z in uparrow x by WAYBEL_0:18; then sup {y,z} in uparrow x by YELLOW_0:41; hence sup {y,z} in the carrier of subrelstr uparrow x by YELLOW_0:def 15; end; then subrelstr uparrow x is join-inheriting by YELLOW_0:def 17; hence uparrow x is join-closed by Def2; end; theorem Th38: for L be Semilattice for x be Element of L holds uparrow x is meet-closed proof let L be Semilattice; let x be Element of L; reconsider x1 = x as Element of L; now let y,z be Element of L; assume that A1: y in the carrier of subrelstr uparrow x and A2: z in the carrier of subrelstr uparrow x and ex_inf_of {y,z},L; y in uparrow x & z in uparrow x by A1,A2,YELLOW_0:def 15; then y >= x1 & z >= x1 by WAYBEL_0:18; then y"/\"z >= x1"/\"x1 by YELLOW_3:2; then y"/\"z >= x1 by YELLOW_5:2; then y"/\"z in uparrow x by WAYBEL_0:18; then inf {y,z} in uparrow x by YELLOW_0:40; hence inf {y,z} in the carrier of subrelstr uparrow x by YELLOW_0:def 15; end; then subrelstr uparrow x is meet-inheriting by YELLOW_0:def 16; hence uparrow x is meet-closed by Def1; end; definition let L be sup-Semilattice; let x be Element of L; cluster downarrow x -> join-closed; coherence by Th35; cluster uparrow x -> join-closed; coherence by Th37; end; definition let L be Semilattice; let x be Element of L; cluster downarrow x -> meet-closed; coherence by Th36; cluster uparrow x -> meet-closed; coherence by Th38; end; theorem Th39: for L be sup-Semilattice for x be Element of L holds waybelow x is join-closed proof let L be sup-Semilattice; let x be Element of L; now let y,z be Element of L; assume that A1: y in the carrier of subrelstr waybelow x and A2: z in the carrier of subrelstr waybelow x and ex_sup_of {y,z},L; y in waybelow x & z in waybelow x by A1,A2,YELLOW_0:def 15; then y << x & z << x by WAYBEL_3:7; then y"\/"z << x by WAYBEL_3:3; then y"\/"z in waybelow x by WAYBEL_3:7; then sup {y,z} in waybelow x by YELLOW_0:41; hence sup {y,z} in the carrier of subrelstr waybelow x by YELLOW_0:def 15; end; then subrelstr waybelow x is join-inheriting by YELLOW_0:def 17; hence waybelow x is join-closed by Def2; end; theorem Th40: for L be Semilattice for x be Element of L holds waybelow x is meet-closed proof let L be Semilattice; let x be Element of L; now let y,z be Element of L; assume that A1: y in the carrier of subrelstr waybelow x and z in the carrier of subrelstr waybelow x and ex_inf_of {y,z},L; y in waybelow x by A1,YELLOW_0:def 15; then A2: y << x by WAYBEL_3:7; y"/\"z <= y by YELLOW_0:23; then y"/\"z << x by A2,WAYBEL_3:2; then y"/\"z in waybelow x by WAYBEL_3:7; then inf {y,z} in waybelow x by YELLOW_0:40; hence inf {y,z} in the carrier of subrelstr waybelow x by YELLOW_0:def 15; end; then subrelstr waybelow x is meet-inheriting by YELLOW_0:def 16; hence waybelow x is meet-closed by Def1; end; theorem Th41: for L be sup-Semilattice for x be Element of L holds wayabove x is join-closed proof let L be sup-Semilattice; let x be Element of L; now let y,z be Element of L; assume that A1: y in the carrier of subrelstr wayabove x and z in the carrier of subrelstr wayabove x and ex_sup_of {y,z},L; y in wayabove x by A1,YELLOW_0:def 15; then A2: y >> x by WAYBEL_3:8; y"\/"z >= y by YELLOW_0:22; then y"\/"z >> x by A2,WAYBEL_3:2; then y"\/"z in wayabove x by WAYBEL_3:8; then sup {y,z} in wayabove x by YELLOW_0:41; hence sup {y,z} in the carrier of subrelstr wayabove x by YELLOW_0:def 15 ; end; then subrelstr wayabove x is join-inheriting by YELLOW_0:def 17; hence wayabove x is join-closed by Def2; end; definition let L be sup-Semilattice; let x be Element of L; cluster waybelow x -> join-closed; coherence by Th39; cluster wayabove x -> join-closed; coherence by Th41; end; definition let L be Semilattice; let x be Element of L; cluster waybelow x -> meet-closed; coherence by Th40; end; begin :: About Bases of Continuous Lattices definition let T be TopStruct; func weight T -> Cardinal equals meet {Card B where B is Basis of T : not contradiction}; coherence proof defpred P[Ordinal] means $1 in {Card B where B is Basis of T : not contradiction}; A1: ex A be Ordinal st P[A] proof take Card the topology of T; the topology of T is Basis of T by CANTOR_1:2; hence thesis; end; consider A be Ordinal such that A2: P[A] and A3: for C be Ordinal st P[C] holds A c= C from Ordinal_Min(A1); consider B be Basis of T such that A4: A = Card B by A2; reconsider A as Cardinal by A4; set X = {Card B1 where B1 is Basis of T : not contradiction}; the topology of T is Basis of T by CANTOR_1:2; then A5: Card the topology of T in X; now let x be set; thus (for y be set holds y in X implies x in y) implies x in A by A2; assume A6: x in A; let y be set; assume A7: y in X; then consider B1 be Basis of T such that A8: y = Card B1; reconsider y1 = y as Cardinal by A8; A c= y1 by A3,A7; hence x in y by A6; end; hence thesis by A5,SETFAM_1:def 1; end; end; definition let T be TopStruct; attr T is second-countable means weight T c= omega; end; definition :: DEFINITION 4.1 let L be continuous sup-Semilattice; mode CLbasis of L -> Subset of L means :Def7: it is join-closed & for x be Element of L holds x = sup (waybelow x /\ it); existence proof take S = [#]L; subrelstr S is join-inheriting by WAYBEL_0:64; hence S is join-closed by Def2; let x be Element of L; thus x = sup waybelow x by WAYBEL_3:def 5 .= sup (waybelow x /\ S) by PRE_TOPC:15; end; end; definition let L be non empty RelStr; let S be Subset of L; attr S is with_bottom means :Def8: Bottom L in S; end; definition let L be non empty RelStr; let S be Subset of L; attr S is with_top means :Def9: Top L in S; end; definition let L be non empty RelStr; cluster with_bottom -> non empty Subset of L; coherence by Def8; end; definition let L be non empty RelStr; cluster with_top -> non empty Subset of L; coherence by Def9; end; definition let L be non empty RelStr; cluster with_bottom Subset of L; existence proof take [#]L; Bottom L in the carrier of L; hence Bottom L in [#]L by PRE_TOPC:12; end; cluster with_top Subset of L; existence proof take [#]L; Top L in the carrier of L; hence Top L in [#]L by PRE_TOPC:12; end; end; definition let L be continuous sup-Semilattice; cluster with_bottom CLbasis of L; existence proof for x,y be Element of L st x in [#]L & y in [#]L holds sup {x,y} in [#]L proof let x,y be Element of L; assume that x in [#]L and y in [#]L; sup {x,y} in the carrier of L; hence sup {x,y} in [#]L by PRE_TOPC:12; end; then A1: [#]L is join-closed by Th18; now let x be Element of L; waybelow x c= the carrier of L; then waybelow x c= [#]L by PRE_TOPC:12; then waybelow x /\ [#]L = waybelow x by XBOOLE_1:28; hence x = sup (waybelow x /\ [#]L) by WAYBEL_3:def 5; end; then reconsider S = [#]L as CLbasis of L by A1,Def7; take S; Bottom L in the carrier of L; then Bottom L in [#]L by PRE_TOPC:12; hence thesis by Def8; end; cluster with_top CLbasis of L; existence proof for x,y be Element of L st x in [#]L & y in [#]L holds sup {x,y} in [#]L proof let x,y be Element of L; assume that x in [#]L and y in [#]L; sup {x,y} in the carrier of L; hence sup {x,y} in [#]L by PRE_TOPC:12; end; then A2: [#]L is join-closed by Th18; now let x be Element of L; waybelow x c= the carrier of L; then waybelow x c= [#]L by PRE_TOPC:12; then waybelow x /\ [#]L = waybelow x by XBOOLE_1:28; hence x = sup (waybelow x /\ [#]L) by WAYBEL_3:def 5; end; then reconsider S = [#]L as CLbasis of L by A2,Def7; take S; Top L in the carrier of L; then Top L in [#]L by PRE_TOPC:12; hence thesis by Def9; end; end; theorem Th42: for L be lower-bounded antisymmetric non empty RelStr for S be with_bottom Subset of L holds subrelstr S is lower-bounded proof let L be lower-bounded antisymmetric non empty RelStr; let S be with_bottom Subset of L; Bottom L in S by Def8; then Bottom L in the carrier of subrelstr S by YELLOW_0:def 15; then reconsider dL = Bottom L as Element of subrelstr S; take dL; now let x be Element of subrelstr S; assume x in the carrier of subrelstr S; reconsider x1 = x as Element of L by YELLOW_0:59; Bottom L <= x1 by YELLOW_0:44; hence dL <= x by YELLOW_0:61; end; hence dL is_<=_than the carrier of subrelstr S by LATTICE3:def 8; end; definition let L be lower-bounded antisymmetric non empty RelStr; let S be with_bottom Subset of L; cluster subrelstr S -> lower-bounded; coherence by Th42; end; definition let L be continuous sup-Semilattice; cluster -> join-closed CLbasis of L; coherence by Def7; end; definition cluster bounded non trivial (continuous LATTICE); existence proof consider X be non empty set; take BoolePoset X; thus thesis; end; end; definition let L be lower-bounded non trivial (continuous sup-Semilattice); cluster -> non empty CLbasis of L; coherence proof let B be CLbasis of L; assume A1: B is empty; Top L = "\/"(waybelow Top L /\ B,L) by Def7 .= Bottom L by A1,YELLOW_0:def 11; hence contradiction by WAYBEL_7:5; end; end; theorem Th43: for L be sup-Semilattice holds the carrier of CompactSublatt L is join-closed Subset of L proof let L be sup-Semilattice; the carrier of CompactSublatt L c= the carrier of L by YELLOW_0:def 13; then reconsider C = the carrier of CompactSublatt L as Subset of L ; subrelstr C = CompactSublatt L by YELLOW_0:def 15; hence the carrier of CompactSublatt L is join-closed Subset of L by Def2; end; theorem Th44: :: Under 4.1 (i) for L be algebraic lower-bounded LATTICE holds the carrier of CompactSublatt L is with_bottom CLbasis of L proof let L be algebraic lower-bounded LATTICE; reconsider C = the carrier of CompactSublatt L as join-closed Subset of L by Th43; now let x be Element of L; x = sup compactbelow x by WAYBEL_8:def 3; hence x = sup (waybelow x /\ C) by Th1; end; then reconsider C as CLbasis of L by Def7; Bottom L in C by WAYBEL_8:3; hence the carrier of CompactSublatt L is with_bottom CLbasis of L by Def8; end; theorem :: Under 4.1 (ii) for L be continuous lower-bounded sup-Semilattice st the carrier of CompactSublatt L is CLbasis of L holds L is algebraic proof let L be continuous lower-bounded sup-Semilattice; A1: for x being Element of L holds compactbelow x is non empty directed; assume A2: the carrier of CompactSublatt L is CLbasis of L; reconsider C = the carrier of CompactSublatt L as Subset of L by Th43; now let x be Element of L; x = sup (waybelow x /\ C) by A2,Def7; hence x = sup compactbelow x by Th1; end; then L is satisfying_axiom_K by WAYBEL_8:def 3; hence L is algebraic by A1,WAYBEL_8:def 4; end; theorem Th46: :: PROPOSITION 4.2. (1) iff (2) for L be continuous lower-bounded LATTICE for B be join-closed Subset of L holds B is CLbasis of L iff for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b << y proof let L be continuous lower-bounded LATTICE; let B be join-closed Subset of L; thus B is CLbasis of L implies for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b << y proof assume A1: B is CLbasis of L; let x,y be Element of L such that A2: not y <= x; thus ex b be Element of L st b in B & not b <= x & b << y proof assume A3: for b1 be Element of L holds not b1 in B or b1 <= x or not b1 << y; A4: ex_sup_of waybelow y /\ B,L & ex_sup_of downarrow x,L by YELLOW_0:17; waybelow y /\ B c= downarrow x proof let z be set; assume A5: z in waybelow y /\ B; then A6: z in waybelow y & z in B by XBOOLE_0:def 3; reconsider z1 = z as Element of L by A5; z1 << y by A6,WAYBEL_3:7; then z1 <= x by A3,A6; hence z in downarrow x by WAYBEL_0:17; end; then sup (waybelow y /\ B) <= sup (downarrow x) by A4,YELLOW_0:34; then y <= sup (downarrow x) by A1,Def7; hence contradiction by A2,WAYBEL_0:34; end; end; assume A7: for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b << y; now let x be Element of L; A8: x = sup waybelow x by WAYBEL_3:def 5; A9: ex_sup_of waybelow x /\ B,L & ex_sup_of waybelow x,L by YELLOW_0:17; waybelow x /\ B c= waybelow x by XBOOLE_1:17; then A10: sup (waybelow x /\ B) <= sup waybelow x by A9,YELLOW_0:34; x <= sup (waybelow x /\ B) proof assume not x <= sup (waybelow x /\ B); then consider b be Element of L such that A11: b in B and A12: not b <= sup (waybelow x /\ B) and A13: b << x by A7; b in waybelow x by A13,WAYBEL_3:7; then b in waybelow x /\ B by A11,XBOOLE_0:def 3; hence contradiction by A12,YELLOW_2:24; end; hence x = sup (waybelow x /\ B) by A8,A10,YELLOW_0:def 3; end; hence B is CLbasis of L by Def7; end; theorem Th47: :: PROPOSITION 4.2. (1) iff (3) for L be continuous lower-bounded LATTICE for B be join-closed Subset of L st Bottom L in B holds B is CLbasis of L iff for x,y be Element of L st x << y ex b be Element of L st b in B & x <= b & b << y proof let L be continuous lower-bounded LATTICE; let B be join-closed Subset of L; assume A1: Bottom L in B; thus B is CLbasis of L implies for x,y be Element of L st x << y ex b be Element of L st b in B & x <= b & b << y proof assume A2: B is CLbasis of L; let x,y be Element of L; assume A3: x << y; A4: waybelow y /\ B is join-closed by Th33; Bottom L << y by WAYBEL_3:4; then Bottom L in waybelow y by WAYBEL_3:7; then reconsider D = waybelow y /\ B as non empty directed Subset of L by A1,A4,Th30,XBOOLE_0:def 3; y = sup D by A2,Def7; then consider b be Element of L such that A5: b in D and A6: x <= b by A3,WAYBEL_3:def 1; take b; b in waybelow y & b in B by A5,XBOOLE_0:def 3; hence thesis by A6,WAYBEL_3:7; end; assume A7: for x,y be Element of L st x << y ex b be Element of L st b in B & x <= b & b << y; now let x be Element of L; waybelow x /\ B c= waybelow x by XBOOLE_1:17; then sup (waybelow x /\ B) <= sup waybelow x by WAYBEL_7:3; then A8: sup (waybelow x /\ B) <= x by WAYBEL_3:def 5; x <= sup (waybelow x /\ B) proof assume A9: not x <= sup (waybelow x /\ B); for x being Element of L holds waybelow x is non empty directed; then consider u be Element of L such that A10: u << x and A11: not u <= sup (waybelow x /\ B) by A9,WAYBEL_3:24; consider b be Element of L such that A12: b in B and A13: u <= b and A14: b << x by A7,A10; b in waybelow x by A14,WAYBEL_3:7; then A15: b in waybelow x /\ B by A12,XBOOLE_0:def 3; A16: sup (waybelow x /\ B) is_>=_than waybelow x /\ B by YELLOW_0:32; not b <= sup (waybelow x /\ B) by A11,A13,YELLOW_0:def 2; hence contradiction by A15,A16,LATTICE3:def 9; end; hence x = sup (waybelow x /\ B) by A8,YELLOW_0:def 3; end; hence B is CLbasis of L by Def7; end; Lm2: for L be continuous lower-bounded LATTICE for B be join-closed Subset of L st Bottom L in B holds (for x,y be Element of L st x << y ex b be Element of L st b in B & x <= b & b << y) implies (the carrier of CompactSublatt L c= B & for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y) proof let L be continuous lower-bounded LATTICE; let B be join-closed Subset of L; assume A1: Bottom L in B; assume A2: for x,y be Element of L st x << y ex b be Element of L st b in B & x <= b & b << y; thus the carrier of CompactSublatt L c= B proof let z be set; assume A3: z in the carrier of CompactSublatt L; the carrier of CompactSublatt L c= the carrier of L by YELLOW_0:def 13; then reconsider z1 = z as Element of L by A3; z1 is compact by A3,WAYBEL_8:def 1; then z1 << z1 by WAYBEL_3:def 2; then consider b be Element of L such that A4: b in B and A5: z1 <= b and A6: b << z1 by A2; b <= z1 by A6,WAYBEL_3:1; hence z in B by A4,A5,YELLOW_0:def 3; end; A7: B is CLbasis of L by A1,A2,Th47; let x,y be Element of L; assume not y <= x; then consider b be Element of L such that A8: b in B and A9: not b <= x and A10: b << y by A7,Th46; take b; thus b in B & not b <= x & b <= y by A8,A9,A10,WAYBEL_3:1; end; Lm3: for L be continuous lower-bounded LATTICE for B be Subset of L holds (for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y) implies (for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b << y) proof let L be continuous lower-bounded LATTICE; let B be Subset of L; assume A1: for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y; let x,y be Element of L; assume A2: not y <= x; for z be Element of L holds waybelow z is non empty directed; then consider y1 be Element of L such that A3: y1 << y and A4: not y1 <= x by A2,WAYBEL_3:24; consider b be Element of L such that A5: b in B and A6: not b <= x and A7: b <= y1 by A1,A4; take b; thus b in B & not b <= x & b << y by A3,A5,A6,A7,WAYBEL_3:2; end; theorem Th48: :: PROPOSITION 4.2. (1) iff (4) for L be continuous lower-bounded LATTICE for B be join-closed Subset of L st Bottom L in B holds B is CLbasis of L iff (the carrier of CompactSublatt L c= B & for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y) proof let L be continuous lower-bounded LATTICE; let B be join-closed Subset of L; assume A1: Bottom L in B; thus B is CLbasis of L implies (the carrier of CompactSublatt L c= B & for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y) proof assume B is CLbasis of L; then for x,y be Element of L st x << y ex b be Element of L st b in B & x <= b & b << y by A1,Th47; hence the carrier of CompactSublatt L c= B & for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y by A1,Lm2; end; assume the carrier of CompactSublatt L c= B & for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y; then for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b << y by Lm3; hence B is CLbasis of L by Th46; end; theorem :: PROPOSITION 4.2. (1) iff (5) for L be continuous lower-bounded LATTICE for B be join-closed Subset of L st Bottom L in B holds B is CLbasis of L iff for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y proof let L be continuous lower-bounded LATTICE; let B be join-closed Subset of L; assume A1: Bottom L in B; thus B is CLbasis of L implies for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y proof assume B is CLbasis of L; then for x,y be Element of L st x << y ex b be Element of L st b in B & x <= b & b << y by A1,Th47; hence for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y by A1,Lm2; end; assume for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b <= y; then for x,y be Element of L st not y <= x ex b be Element of L st b in B & not b <= x & b << y by Lm3; hence B is CLbasis of L by Th46; end; theorem Th50: for L be lower-bounded sup-Semilattice for S be non empty full SubRelStr of L st Bottom L in the carrier of S & the carrier of S is join-closed Subset of L for x be Element of L holds waybelow x /\ (the carrier of S) is Ideal of S proof let L be lower-bounded sup-Semilattice; let S be non empty full SubRelStr of L; assume that A1: Bottom L in the carrier of S and A2: the carrier of S is join-closed Subset of L; let x be Element of L; A3: waybelow x /\ (the carrier of S) c= the carrier of S by XBOOLE_1:17; Bottom L << x by WAYBEL_3:4; then Bottom L in waybelow x by WAYBEL_3:7; then reconsider X = waybelow x /\ (the carrier of S) as non empty Subset of S by A1,A3,XBOOLE_0:def 3; A4: now let a,b be Element of S; reconsider a1 = a, b1 = b as Element of L by YELLOW_0:59; assume that A5: a in X and A6: b <= a; A7: b1 <= a1 by A6,YELLOW_0:60; a in waybelow x by A5,XBOOLE_0:def 3; then a1 << x by WAYBEL_3:7; then b1 << x by A7,WAYBEL_3:2; then b in waybelow x by WAYBEL_3:7; hence b in X by XBOOLE_0:def 3; end; reconsider S1 = the carrier of S as join-closed Subset of L by A2; waybelow x /\ S1 is join-closed by Th33; then waybelow x /\ S1 is directed by Th30; hence thesis by A4,WAYBEL10:24,WAYBEL_0:def 19; end; definition let L be non empty reflexive transitive RelStr; let S be non empty full SubRelStr of L; func supMap S -> map of InclPoset(Ids S), L means :Def10: for I be Ideal of S holds it.I = "\/"(I,L); existence proof set P = InclPoset Ids S; deffunc F(set) = "\/"($1,L); A1: for I be set st I in the carrier of P holds F(I) in the carrier of L; ex f be Function of the carrier of P, the carrier of L st for I be set st I in the carrier of P holds f.I = F(I) from Lambda1(A1); then consider f be Function of the carrier of P,the carrier of L such that A2: for I be set st I in the carrier of P holds f.I = "\/"(I,L); reconsider f as map of P,L; take f; for I be Ideal of S holds f.I = "\/"(I,L) proof let I be Ideal of S; I in { X where X is Ideal of S : not contradiction }; then I in the carrier of RelStr(#Ids S, RelIncl Ids S#) by WAYBEL_0:def 23; then I in the carrier of P by YELLOW_1:def 1; hence f.I = "\/"(I,L) by A2; end; hence thesis; end; uniqueness proof let f,g be map of InclPoset Ids S, L; assume that A3: for I be Ideal of S holds f.I = "\/"(I,L) and A4: for I be Ideal of S holds g.I = "\/"(I,L); set P = InclPoset Ids S; A5: dom f = the carrier of P & dom g = the carrier of P by FUNCT_2:def 1; A6: the carrier of P = the carrier of RelStr(#Ids S, RelIncl Ids S#) by YELLOW_1:def 1 .= Ids S; now let x be set; assume x in the carrier of P; then x in { X where X is Ideal of S : not contradiction } by A6,WAYBEL_0:def 23; then ex I be Ideal of S st x = I; then reconsider I = x as Ideal of S; f.I = "\/"(I,L) & g.I = "\/"(I,L) by A3,A4; hence f.x = g.x; end; hence f = g by A5,FUNCT_1:9; end; end; definition let L be non empty reflexive transitive RelStr; let S be non empty full SubRelStr of L; func idsMap S -> map of InclPoset(Ids S), InclPoset(Ids L) means :Def11: for I be Ideal of S ex J be Subset of L st I = J & it.I = downarrow J; existence proof set P = InclPoset Ids S; set R = InclPoset Ids L; deffunc F(Subset of L) = downarrow $1; defpred P[set,set] means ex J be Subset of L st $1 = J & $2 = downarrow J; A1: for I be Element of P ex K be Element of R st P[I,K] proof let I be Element of P; I in the carrier of P; then I in Ids S by YELLOW_1:1; then I in { X where X is Ideal of S : not contradiction } by WAYBEL_0:def 23; then consider J be Ideal of S such that A2: J = I; reconsider J as non empty directed Subset of L by YELLOW_2:7; downarrow J in { X where X is Ideal of L : not contradiction }; then downarrow J in Ids L by WAYBEL_0:def 23; then reconsider K = downarrow J as Element of R by YELLOW_1:1; take K,J; thus thesis by A2; end; ex f be Function of the carrier of P, the carrier of R st for I be Element of P holds P[I,f.I] from FuncExD(A1); then consider f be Function of the carrier of P,the carrier of R such that A3: for I be Element of P ex J be Subset of L st I = J & f.I = downarrow J; reconsider f as map of P,R; take f; for I be Ideal of S ex J be Subset of L st I = J & f.I = downarrow J proof let I be Ideal of S; I in { X where X is Ideal of S : not contradiction }; then I in the carrier of RelStr(#Ids S, RelIncl Ids S#) by WAYBEL_0:def 23; then I in the carrier of P by YELLOW_1:def 1; then consider J be Subset of L such that A4: I = J and A5: f.I = downarrow J by A3; reconsider J as Subset of L; take J; thus thesis by A4,A5; end; hence thesis; end; uniqueness proof let f,g be map of InclPoset Ids S, InclPoset Ids L; assume that A6: for I be Ideal of S ex J be Subset of L st I = J & f.I = downarrow J and A7: for I be Ideal of S ex J be Subset of L st I = J & g.I = downarrow J; set P = InclPoset Ids S; A8: dom f = the carrier of P & dom g = the carrier of P by FUNCT_2:def 1; A9: the carrier of P = the carrier of RelStr(#Ids S, RelIncl Ids S#) by YELLOW_1:def 1 .= Ids S; now let x be set; assume x in the carrier of P; then x in { X where X is Ideal of S : not contradiction } by A9,WAYBEL_0:def 23; then ex I be Ideal of S st x = I; then reconsider I = x as Ideal of S; consider J1 be Subset of L such that A10: I = J1 and A11: f.I = downarrow J1 by A6; consider J2 be Subset of L such that A12: I = J2 and A13: g.I = downarrow J2 by A7; thus f.x = g.x by A10,A11,A12,A13; end; hence f = g by A8,FUNCT_1:9; end; end; definition let L be reflexive RelStr; let B be Subset of L; cluster subrelstr B -> reflexive; coherence; end; definition let L be transitive RelStr; let B be Subset of L; cluster subrelstr B -> transitive; coherence; end; definition let L be antisymmetric RelStr; let B be Subset of L; cluster subrelstr B -> antisymmetric; coherence; end; definition let L be lower-bounded continuous sup-Semilattice; let B be with_bottom CLbasis of L; func baseMap B -> map of L, InclPoset(Ids subrelstr B) means :Def12: for x be Element of L holds it.x = waybelow x /\ B; existence proof set P = InclPoset Ids subrelstr B; defpred P[set,set] means ex y be Element of L st $1 = y & $2 = waybelow y /\ B; A1: for x be Element of L ex z be Element of P st P[x,z] proof let x be Element of L; reconsider y = x as Element of L; A2: the carrier of subrelstr B = B by YELLOW_0:def 15; Bottom L in B by Def8; then waybelow y /\ B is Ideal of subrelstr B by A2,Th50; then reconsider z = waybelow y /\ B as Element of P by YELLOW_2:43; take z,y; thus thesis; end; ex f be Function of the carrier of L, the carrier of P st for x be Element of L holds P[x,f.x] from FuncExD(A1); then consider f be Function of the carrier of L,the carrier of P such that A3: for x be Element of L ex y be Element of L st x = y & f.x = waybelow y /\ B; reconsider f as map of L,P; take f; now let x be Element of L; consider y be Element of L such that A4: x = y and A5: f.x = waybelow y /\ B by A3; thus f.x = waybelow x /\ B by A4,A5; end; hence thesis; end; uniqueness proof let f,g be map of L,InclPoset Ids subrelstr B; assume that A6: for x be Element of L holds f.x = waybelow x /\ B and A7: for x be Element of L holds g.x = waybelow x /\ B; A8: dom f = the carrier of L & dom g = the carrier of L by FUNCT_2:def 1; now let z be set; assume z in the carrier of L; then reconsider z1 = z as Element of L; f.z = waybelow z1 /\ B & g.z = waybelow z1 /\ B by A6,A7; hence f.z = g.z; end; hence f = g by A8,FUNCT_1:9; end; end; theorem Th51: for L be non empty reflexive transitive RelStr for S be non empty full SubRelStr of L holds dom supMap S = Ids S & rng supMap S is Subset of L proof let L be non empty reflexive transitive RelStr; let S be non empty full SubRelStr of L; set P = InclPoset Ids S; thus dom(supMap S) = the carrier of P by FUNCT_2:def 1 .= the carrier of RelStr(#Ids S, RelIncl Ids S#) by YELLOW_1:def 1 .= Ids S; thus rng supMap S is Subset of L; end; theorem Th52: for L be non empty reflexive transitive RelStr for S be non empty full SubRelStr of L for x be set holds x in dom supMap S iff x is Ideal of S proof let L be non empty reflexive transitive RelStr; let S be non empty full SubRelStr of L; let x be set; hereby assume x in dom supMap S; then x in Ids S by Th51; then x in { X where X is Ideal of S : not contradiction } by WAYBEL_0:def 23; then ex I be Ideal of S st x = I; hence x is Ideal of S; end; assume x is Ideal of S; then x in { X where X is Ideal of S: not contradiction }; then x in Ids S by WAYBEL_0:def 23; hence x in dom supMap S by Th51; end; theorem Th53: for L be non empty reflexive transitive RelStr for S be non empty full SubRelStr of L holds dom idsMap S = Ids S & rng idsMap S is Subset of Ids L proof let L be non empty reflexive transitive RelStr; let S be non empty full SubRelStr of L; set P = InclPoset Ids S; thus dom(idsMap S) = the carrier of P by FUNCT_2:def 1 .= the carrier of RelStr(#Ids S, RelIncl Ids S#) by YELLOW_1:def 1 .= Ids S; thus rng idsMap S is Subset of Ids L by YELLOW_1:1; end; theorem Th54: for L be non empty reflexive transitive RelStr for S be non empty full SubRelStr of L for x be set holds x in dom idsMap S iff x is Ideal of S proof let L be non empty reflexive transitive RelStr; let S be non empty full SubRelStr of L; let x be set; hereby assume x in dom idsMap S; then x in Ids S by Th53; then x in { X where X is Ideal of S : not contradiction } by WAYBEL_0:def 23; then ex I be Ideal of S st x = I; hence x is Ideal of S; end; assume x is Ideal of S; then x in { X where X is Ideal of S: not contradiction }; then x in Ids S by WAYBEL_0:def 23; hence x in dom idsMap S by Th53; end; theorem Th55: for L be non empty reflexive transitive RelStr for S be non empty full SubRelStr of L for x be set holds x in rng idsMap S implies x is Ideal of L proof let L be non empty reflexive transitive RelStr; let S be non empty full SubRelStr of L; let x be set; assume A1: x in rng idsMap S; rng idsMap S is Subset of Ids L by Th53; then x in Ids L by A1; then x in { X where X is Ideal of L : not contradiction } by WAYBEL_0:def 23; then ex I be Ideal of L st x = I; hence x is Ideal of L; end; theorem Th56: for L be lower-bounded continuous sup-Semilattice for B be with_bottom CLbasis of L holds dom baseMap B = the carrier of L & rng baseMap B is Subset of Ids subrelstr B proof let L be lower-bounded continuous sup-Semilattice; let B be with_bottom CLbasis of L; thus dom(baseMap B) = the carrier of L by FUNCT_2:def 1; thus rng baseMap B is Subset of Ids subrelstr B by YELLOW_1:1; end; theorem for L be lower-bounded continuous sup-Semilattice for B be with_bottom CLbasis of L for x be set holds x in rng baseMap B implies x is Ideal of subrelstr B proof let L be lower-bounded continuous sup-Semilattice; let B be with_bottom CLbasis of L; let x be set; assume A1: x in rng baseMap B; rng baseMap B is Subset of Ids subrelstr B by Th56; then x in Ids subrelstr B by A1; then x in { X where X is Ideal of subrelstr B : not contradiction } by WAYBEL_0:def 23; then ex I be Ideal of subrelstr B st x = I; hence x is Ideal of subrelstr B; end; theorem Th58: for L be up-complete (non empty Poset) for S be non empty full SubRelStr of L holds supMap S is monotone proof let L be up-complete (non empty Poset); let S be non empty full SubRelStr of L; set f = supMap S; now let x, y be Element of InclPoset Ids S; assume A1: x <= y; reconsider I = x, J = y as Ideal of S by YELLOW_2:43; I is non empty directed Subset of L & J is non empty directed Subset of L by YELLOW_2:7; then A2: ex_sup_of I,L & ex_sup_of J,L by WAYBEL_0:75; A3: I c= J by A1,YELLOW_1:3; f.x = "\/"(I,L) & f.y = "\/"(J,L) by Def10; hence f.x <= f.y by A2,A3,YELLOW_0:34; end; hence thesis by WAYBEL_1:def 2; end; theorem Th59: for L be non empty reflexive transitive RelStr for S be non empty full SubRelStr of L holds idsMap S is monotone proof let L be non empty reflexive transitive RelStr; let S be non empty full SubRelStr of L; set f = idsMap S; now let x, y be Element of InclPoset Ids S; assume A1: x <= y; reconsider I = x, J = y as Ideal of S by YELLOW_2:43; consider K1 be Subset of L such that A2: I = K1 and A3: f.x = downarrow K1 by Def11; consider K2 be Subset of L such that A4: J = K2 and A5: f.y = downarrow K2 by Def11; I c= J by A1,YELLOW_1:3; then downarrow K1 c= downarrow K2 by A2,A4,YELLOW_3:6; hence f.x <= f.y by A3,A5,YELLOW_1:3; end; hence thesis by WAYBEL_1:def 2; end; theorem Th60: for L be lower-bounded continuous sup-Semilattice for B be with_bottom CLbasis of L holds baseMap B is monotone proof let L be lower-bounded continuous sup-Semilattice; let B be with_bottom CLbasis of L; set f = baseMap B; now let x, y be Element of L; assume A1: x <= y; A2: f.x = waybelow x /\ B by Def12; A3: f.y = waybelow y /\ B by Def12; waybelow x c= waybelow y by A1,WAYBEL_3:12; then f.x c= f.y by A2,A3,XBOOLE_1:26; hence f.x <= f.y by YELLOW_1:3; end; hence thesis by WAYBEL_1:def 2; end; definition let L be up-complete (non empty Poset); let S be non empty full SubRelStr of L; cluster supMap S -> monotone; coherence by Th58; end; definition let L be non empty reflexive transitive RelStr; let S be non empty full SubRelStr of L; cluster idsMap S -> monotone; coherence by Th59; end; definition let L be lower-bounded continuous sup-Semilattice; let B be with_bottom CLbasis of L; cluster baseMap B -> monotone; coherence by Th60; end; theorem Th61: for L be lower-bounded (continuous sup-Semilattice) for B be with_bottom CLbasis of L holds idsMap (subrelstr B) is sups-preserving proof let L be lower-bounded (continuous sup-Semilattice); let B be with_bottom CLbasis of L; Bottom L in B by Def8; then A1: Bottom L in the carrier of subrelstr B by YELLOW_0:def 15; A2: subrelstr B is join-inheriting by Def2; set f = idsMap (subrelstr B); now let X be Subset of InclPoset Ids subrelstr B; reconsider supX = sup X as Ideal of subrelstr B by YELLOW_2:43; reconsider unionX = union X as Subset of L by WAYBEL13:3; consider J be Subset of L such that A3: supX = J and A4: f.supX = downarrow J by Def11; reconsider dfuX = downarrow finsups union X as Subset of L by WAYBEL13:3; reconsider fuX = finsups union X as Subset of L by WAYBEL13:3; now assume ex_sup_of X,InclPoset Ids subrelstr B; thus ex_sup_of f.:X,InclPoset Ids L by YELLOW_0:17; A5: downarrow finsups union (f.:X) c= downarrow dfuX proof let x be set; assume A6: x in downarrow finsups union (f.:X); then reconsider x1 = x as Element of L; consider y1 be Element of L such that A7: y1 >= x1 and A8: y1 in finsups union (f.:X) by A6,WAYBEL_0:def 15; y1 in { "\/"(V,L) where V is finite Subset of union (f.:X) : ex_sup_of V,L } by A8,WAYBEL_0:def 27; then consider Y be finite Subset of union (f.:X) such that A9: y1 = "\/"(Y,L) and ex_sup_of Y,L; defpred P[set,set] means ex I be Element of InclPoset Ids subrelstr B, z1,z2 be Element of L st z1 = $1 & z2 = $2 & I in X & $2 in I & z1 <= z2; A10: for z be set st z in Y ex v be Element of B st P[z,v] proof let z be set; assume z in Y; then consider J be set such that A11: z in J and A12: J in f.:X by TARSKI:def 4; consider I be set such that I in dom f and A13: I in X and A14: J = f.I by A12,FUNCT_1:def 12; reconsider I as Element of InclPoset Ids subrelstr B by A13; reconsider I1 = I as Ideal of subrelstr B by YELLOW_2:43; f.I is Element of InclPoset Ids L; then reconsider J as Element of InclPoset Ids L by A14; J is Ideal of L by YELLOW_2:43; then reconsider z1 = z as Element of L by A11; consider I2 be Subset of L such that A15: I1 = I2 and A16: f.I1 = downarrow I2 by Def11; consider z2 be Element of L such that A17: z2 >= z1 and A18: z2 in I2 by A11,A14,A16,WAYBEL_0:def 15; reconsider v = z2 as Element of B by A15,A18,YELLOW_0:def 15; take v,I,z1,z2; thus z1 = z & z2 = v & I in X & v in I & z1 <= z2 by A13,A15,A17,A18; end; consider g be Function of Y,B such that A19: for z be set st z in Y holds P[z,g.z] from NonUniqFuncDEx(A10); reconsider srg = "\/"(rng g,subrelstr B) as Element of L by YELLOW_0:59; rng g c= B by RELSET_1:12; then A20: rng g c= the carrier of subrelstr B by YELLOW_0:def 15; A21: dom g = Y by FUNCT_2:def 1; then reconsider Z = rng g as finite Subset of subrelstr B by A20,FINSET_1:26; A22: ex_sup_of Z,subrelstr B proof per cases; suppose Z is non empty; hence thesis by YELLOW_0:54; suppose Z is empty; hence thesis by YELLOW_0:42; end; A23: ex_sup_of Z,L by YELLOW_0:17; "\/"(Z,L) in the carrier of subrelstr B proof per cases; suppose Z is non empty; hence thesis by A2,WAYBEL21:15; suppose Z is empty; hence thesis by A1,YELLOW_0:def 11; end; then reconsider xl = "\/"(Z,L) as Element of subrelstr B ; A24: "\/"(Z, L) is_>=_than Z & for b be Element of L st b is_>=_than Z holds "\/"(Z, L) <= b by A23,YELLOW_0:30; A25: xl is_>=_than Z proof let b be Element of subrelstr B; reconsider b1 = b as Element of L by YELLOW_0:59; assume b in Z; then b1 <= "\/"(Z, L) by A24,LATTICE3:def 9; hence b <= xl by YELLOW_0:61; end; now let b be Element of subrelstr B; reconsider b1 = b as Element of L by YELLOW_0:59; assume A26: b is_>=_than Z; b1 is_>=_than Z proof let c1 be Element of L; assume A27: c1 in Z; then reconsider c = c1 as Element of subrelstr B; c <= b by A26,A27,LATTICE3:def 9; hence c1 <= b1 by YELLOW_0:60; end; then "\/"(Z, L) <= b1 by A23,YELLOW_0:30; hence xl <= b by YELLOW_0:61; end; then A28: "\/"(Z,subrelstr B) = "\/"(Z,L) by A25,YELLOW_0:30; "\/"(rng g,L) is_>=_than Y proof let a be Element of L; assume A29: a in Y; then consider I be Element of InclPoset Ids subrelstr B, a1,a2 be Element of L such that A30: a1 = a and A31: a2 = g.a and I in X and g.a in I and A32: a1 <= a2 by A19; A33: g.a in rng g by A21,A29,FUNCT_1:def 5; "\/"(rng g,L) is_>=_than rng g by YELLOW_0:32; then a2 <= "\/"(rng g,L) by A31,A33,LATTICE3:def 9; hence a <= "\/"(rng g,L) by A30,A32,YELLOW_0:def 2; end; then "\/"(Y,L) <= srg by A28,YELLOW_0:32; then A34: x1 <= srg by A7,A9,YELLOW_0:def 2; A35: finsups union X c= downarrow finsups union X by WAYBEL_0:16; rng g c= union X proof let a be set; assume a in rng g; then consider b be set such that A36: b in dom g and A37: a = g.b by FUNCT_1:def 5; consider I be Element of InclPoset Ids subrelstr B, b1,b2 be Element of L such that b1 = b and b2 = g.b and A38: I in X and A39: g.b in I and b1 <= b2 by A19,A21,A36; thus a in union X by A37,A38,A39,TARSKI:def 4; end; then "\/"(Z,subrelstr B) in { "\/"(V,subrelstr B) where V is finite Subset of union X : ex_sup_of V,subrelstr B } by A22; then "\/"(rng g,subrelstr B) in finsups union X by WAYBEL_0:def 27; hence x in downarrow dfuX by A34,A35,WAYBEL_0:def 15; end; now let x be set; assume A40: x in X; then A41: x in the carrier of InclPoset Ids subrelstr B; x is Element of InclPoset Ids subrelstr B by A40; then reconsider x1 = x as Ideal of subrelstr B by YELLOW_2:43; consider x2 be Subset of L such that A42: x1 = x2 and A43: f.x1 = downarrow x2 by Def11; x1 in dom f by A41,FUNCT_2:def 1; then A44: f.x1 in f.:X by A40,FUNCT_1:def 12; thus x c= union (f.:X) proof let y be set; assume A45: y in x; x c= downarrow x2 by A42,WAYBEL_0:16; hence y in union (f.:X) by A43,A44,A45,TARSKI:def 4; end; end; then union X c= union (f.:X) by ZFMISC_1:94; then A46: finsups unionX c= finsups union (f.:X) by Th2; finsups union X c= finsups unionX by A1,A2,Th5; then finsups union X c= finsups union (f.:X) by A46,XBOOLE_1:1; then A47: downarrow fuX c= downarrow finsups union (f.:X) by YELLOW_3:6; downarrow finsups union X c= downarrow fuX by Th11; then dfuX c= downarrow finsups union (f.:X) by A47,XBOOLE_1:1; then downarrow dfuX c= downarrow downarrow finsups union (f.:X) by YELLOW_3:6; then A48: downarrow dfuX c= downarrow finsups union (f.:X) by Th7; thus sup (f.:X) = downarrow finsups union (f.:X) by Th6 .= downarrow dfuX by A5,A48,XBOOLE_0:def 10 .= f.sup X by A3,A4,Th6; end; hence f preserves_sup_of X by WAYBEL_0:def 31; end; hence idsMap (subrelstr B) is sups-preserving by WAYBEL_0:def 33; end; theorem Th62: for L be up-complete (non empty Poset) for S be non empty full SubRelStr of L holds supMap S = (SupMap L)*(idsMap S) proof let L be up-complete (non empty Poset); let S be non empty full SubRelStr of L; A1: now let x be set; thus x in dom (supMap S) implies x in dom (idsMap S) & (idsMap S).x in dom (SupMap L) proof assume x in dom (supMap S); then x is Ideal of S by Th52; hence x in dom (idsMap S) by Th54; then (idsMap S).x in rng (idsMap S) by FUNCT_1:def 5; then (idsMap S).x is Ideal of L by Th55; hence (idsMap S).x in dom (SupMap L) by YELLOW_2:52; end; thus x in dom (idsMap S) & (idsMap S).x in dom (SupMap L) implies x in dom (supMap S) proof assume that A2: x in dom (idsMap S) and (idsMap S).x in dom (SupMap L); x is Ideal of S by A2,Th54; hence x in dom (supMap S) by Th52; end; end; now let x be set; assume x in dom (supMap S); then reconsider I = x as Ideal of S by Th52; consider J be Subset of L such that A3: I = J and A4: (idsMap S).I = downarrow J by Def11; reconsider J as non empty directed Subset of L by A3,YELLOW_2:7; A5: ex_sup_of J,L by WAYBEL_0:75; thus (supMap S).x = "\/"(I,L) by Def10 .= sup (downarrow J) by A3,A5,WAYBEL_0:33 .= (SupMap L).((idsMap S).x) by A4,YELLOW_2:def 3; end; hence supMap S = (SupMap L)*(idsMap S) by A1,FUNCT_1:20; end; theorem Th63: :: PROPOSITION 4.3.(i) for L be lower-bounded continuous sup-Semilattice for B be with_bottom CLbasis of L holds [supMap subrelstr B,baseMap B] is Galois proof let L be lower-bounded continuous sup-Semilattice; let B be with_bottom CLbasis of L; now let x be Element of L, y be Element of InclPoset Ids subrelstr B; reconsider I = y as Ideal of subrelstr B by YELLOW_2:43; reconsider J = I as non empty directed Subset of L by YELLOW_2:7; A1: ex_sup_of J,L & ex_sup_of waybelow x,L & ex_sup_of downarrow J,L & ex_sup_of waybelow x /\ B,L by YELLOW_0:17; thus x <= (supMap subrelstr B).y implies (baseMap B).x <= y proof assume x <= (supMap subrelstr B).y; then x <= "\/"(I,L) by Def10; then A2: x <= sup downarrow J by A1,WAYBEL_0:33; waybelow x c= downarrow J proof let z be set; assume A3: z in waybelow x; then reconsider z1 = z as Element of L; z1 << x by A3,WAYBEL_3:7; hence z in downarrow J by A2,WAYBEL_3:20; end; then A4: waybelow x /\ B c= downarrow J /\ B by XBOOLE_1:26; downarrow J /\ B c= J proof let z be set; assume A5: z in downarrow J /\ B; then A6: z in downarrow J & z in B by XBOOLE_0:def 3; reconsider z1 = z as Element of L by A5; z in the carrier of subrelstr B by A6,YELLOW_0:def 15; then reconsider z2 = z as Element of subrelstr B; consider v1 be Element of L such that A7: v1 >= z1 and A8: v1 in J by A6,WAYBEL_0:def 15; reconsider v2 = v1 as Element of subrelstr B by A8; z2 <= v2 by A7,YELLOW_0:61; hence z in J by A8,WAYBEL_0:def 19; end; then waybelow x /\ B c= y by A4,XBOOLE_1:1; then (baseMap B).x c= y by Def12; hence (baseMap B).x <= y by YELLOW_1:3; end; thus (baseMap B).x <= y implies x <= (supMap subrelstr B).y proof assume (baseMap B).x <= y; then (baseMap B).x c= y by YELLOW_1:3; then waybelow x /\ B c= y by Def12; then sup (waybelow x /\ B) <= sup J by A1,YELLOW_0:34; then x <= "\/"(I,L) by Def7; hence x <= (supMap subrelstr B).y by Def10; end; end; hence [supMap subrelstr B,baseMap B] is Galois by WAYBEL_1:9; end; theorem Th64: :: PROPOSITION 4.3.(ii) for L be lower-bounded continuous sup-Semilattice for B be with_bottom CLbasis of L holds supMap subrelstr B is upper_adjoint & baseMap B is lower_adjoint proof let L be lower-bounded continuous sup-Semilattice; let B be with_bottom CLbasis of L; [supMap subrelstr B,baseMap B] is Galois by Th63; hence thesis by WAYBEL_1:10; end; theorem Th65: :: PROPOSITION 4.3.(iii) for L be lower-bounded (continuous sup-Semilattice) for B be with_bottom CLbasis of L holds rng supMap subrelstr B = the carrier of L proof let L be lower-bounded (continuous sup-Semilattice); let B be with_bottom CLbasis of L; A1: Bottom L in B by Def8; thus rng supMap subrelstr B = the carrier of L proof thus rng supMap subrelstr B c= the carrier of L; let x be set; assume x in the carrier of L; then reconsider x1 = x as Element of L; set z = waybelow x1 /\ B; z is Subset of B by XBOOLE_1:17; then z is Subset of subrelstr B by YELLOW_0:def 15; then reconsider z as Subset of subrelstr B; Bottom L << x1 by WAYBEL_3:4; then A2: Bottom L in waybelow x1 by WAYBEL_3:7; A3: now let a,b be Element of subrelstr B; reconsider a1 = a, b1 = b as Element of L by YELLOW_0:59; assume that A4: a in z and A5: b <= a; b in the carrier of subrelstr B; then A6: b in B by YELLOW_0:def 15; A7: b1 <= a1 by A5,YELLOW_0:60; a in waybelow x1 by A4,XBOOLE_0:def 3; then a1 << x1 by WAYBEL_3:7; then b1 << x1 by A7,WAYBEL_3:2; then b in waybelow x1 by WAYBEL_3:7; hence b in z by A6,XBOOLE_0:def 3; end; waybelow x1 /\ B is join-closed by Th33; then waybelow x1 /\ B is directed by Th30; then reconsider z as Ideal of subrelstr B by A1,A2,A3,WAYBEL10:24,WAYBEL_0:def 19,XBOOLE_0:def 3; z in { X where X is Ideal of subrelstr B : not contradiction }; then z in Ids subrelstr B by WAYBEL_0:def 23; then A8: z in dom supMap subrelstr B by Th51; x = "\/"(z,L) by Def7 .= (supMap subrelstr B).z by Def10; hence x in rng supMap subrelstr B by A8,FUNCT_1:def 5; end; end; theorem Th66: :: PROPOSITION 4.3.(iv) for L be lower-bounded (continuous sup-Semilattice) for B be with_bottom CLbasis of L holds supMap (subrelstr B) is infs-preserving sups-preserving proof let L be lower-bounded (continuous sup-Semilattice); let B be with_bottom CLbasis of L; supMap (subrelstr B) is upper_adjoint by Th64; hence supMap (subrelstr B) is infs-preserving by WAYBEL_1:13; A1: idsMap (subrelstr B) is sups-preserving by Th61; A2: supMap (subrelstr B) = (SupMap L)*(idsMap (subrelstr B)) by Th62; SupMap L is sups-preserving by WAYBEL13:33; hence supMap (subrelstr B) is sups-preserving by A1,A2,WAYBEL20:28; end; theorem Th67: for L be lower-bounded continuous sup-Semilattice for B be with_bottom CLbasis of L holds baseMap B is sups-preserving proof let L be lower-bounded continuous sup-Semilattice; let B be with_bottom CLbasis of L; baseMap B is lower_adjoint by Th64; hence baseMap B is sups-preserving by WAYBEL_1:14; end; definition let L be lower-bounded continuous sup-Semilattice; let B be with_bottom CLbasis of L; cluster supMap subrelstr B -> infs-preserving sups-preserving; coherence by Th66; cluster baseMap B -> sups-preserving; coherence by Th67; end; canceled; theorem Th69: :: PROPOSITION 4.3.(vi) for L be lower-bounded (continuous sup-Semilattice) for B be with_bottom CLbasis of L holds the carrier of CompactSublatt InclPoset(Ids subrelstr B) = { downarrow b where b is Element of subrelstr B : not contradiction } proof let L be lower-bounded (continuous sup-Semilattice); let B be with_bottom CLbasis of L; thus the carrier of CompactSublatt InclPoset(Ids subrelstr B) c= { downarrow b where b is Element of subrelstr B : not contradiction } proof let x be set; assume A1: x in the carrier of CompactSublatt InclPoset(Ids subrelstr B); the carrier of CompactSublatt InclPoset(Ids subrelstr B) c= the carrier of InclPoset(Ids subrelstr B) by YELLOW_0:def 13; then reconsider x1 = x as Element of InclPoset(Ids subrelstr B) by A1; x1 is compact by A1,WAYBEL_8:def 1; then ex b be Element of subrelstr B st x1 = downarrow b by WAYBEL13:12; hence x in { downarrow b where b is Element of subrelstr B : not contradiction }; end; thus { downarrow b where b is Element of subrelstr B : not contradiction } c= the carrier of CompactSublatt InclPoset(Ids subrelstr B) proof let x be set; assume x in { downarrow b where b is Element of subrelstr B : not contradiction }; then consider b be Element of subrelstr B such that A2: x = downarrow b; reconsider x1 = x as Element of InclPoset(Ids subrelstr B) by A2,YELLOW_2:43; x1 is compact by A2,WAYBEL13:12; hence x in the carrier of CompactSublatt InclPoset(Ids subrelstr B) by WAYBEL_8:def 1; end; end; theorem :: PROPOSITION 4.3.(vii) for L be lower-bounded (continuous sup-Semilattice) for B be with_bottom CLbasis of L holds CompactSublatt InclPoset(Ids subrelstr B),subrelstr B are_isomorphic proof let L be lower-bounded (continuous sup-Semilattice); let B be with_bottom CLbasis of L; deffunc F(Element of subrelstr B) = downarrow $1; A1: for x be Element of subrelstr B holds F(x) is Element of CompactSublatt InclPoset Ids subrelstr B proof let x be Element of subrelstr B; downarrow x in { downarrow b where b is Element of subrelstr B : not contradiction }; then downarrow x in the carrier of CompactSublatt InclPoset Ids subrelstr B by Th69; hence downarrow x is Element of CompactSublatt InclPoset Ids subrelstr B ; end; consider f be map of subrelstr B,CompactSublatt InclPoset Ids subrelstr B such that A2: for x be Element of subrelstr B holds f.x = F(x) from KappaMD(A1); f is isomorphic by A2,WAYBEL13:13; then subrelstr B,CompactSublatt InclPoset(Ids subrelstr B) are_isomorphic by WAYBEL_1:def 8; hence CompactSublatt InclPoset(Ids subrelstr B),subrelstr B are_isomorphic by WAYBEL_1:7; end; Lm4: for L be continuous lower-bounded LATTICE holds L is algebraic implies the carrier of CompactSublatt L is with_bottom CLbasis of L & for B be with_bottom CLbasis of L holds the carrier of CompactSublatt L c= B proof let L be continuous lower-bounded LATTICE; assume L is algebraic; hence the carrier of CompactSublatt L is with_bottom CLbasis of L by Th44; let B be with_bottom CLbasis of L; Bottom L in B by Def8; hence the carrier of CompactSublatt L c= B by Th48; end; theorem Th71: for L be continuous lower-bounded LATTICE for B be with_bottom CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1 for J be Element of InclPoset Ids subrelstr B holds J = waybelow "\/"(J,L) /\ B proof let L be continuous lower-bounded LATTICE; let B be with_bottom CLbasis of L; assume A1: for B1 be with_bottom CLbasis of L holds B c= B1; let J be Element of InclPoset Ids subrelstr B; reconsider J1 = J as Ideal of subrelstr B by YELLOW_2:43; reconsider J2 = J1 as non empty directed Subset of L by YELLOW_2:7; set x = "\/"(J,L); A2: waybelow x /\ B c= J proof let a be set; assume A3: a in waybelow x /\ B; then A4: a in waybelow x & a in B by XBOOLE_0:def 3; reconsider a1 = a as Element of L by A3; a in the carrier of subrelstr B by A4,YELLOW_0:def 15; then reconsider a2 = a as Element of subrelstr B; a1 << x by A4,WAYBEL_3:7; then consider d1 be Element of L such that A5: d1 in J2 and A6: a1 <= d1 by WAYBEL_3:def 1; reconsider d2 = d1 as Element of subrelstr B by A5; a2 <= d2 by A6,YELLOW_0:61; hence a in J by A5,WAYBEL_0:def 19; end; set C = (B \ J2) \/ (waybelow x /\ B); A7: B \ J2 c= B by XBOOLE_1:36; waybelow x /\ B c= B by XBOOLE_1:17; then A8: C c= B by A7,XBOOLE_1:8; A9: subrelstr B is join-inheriting by Def2; subrelstr C is join-inheriting proof let a,b be Element of L; assume that A10: a in the carrier of subrelstr C and A11: b in the carrier of subrelstr C and A12: ex_sup_of {a,b},L; A13: a in C & b in C by A10,A11,YELLOW_0:def 15; then a in B & b in B by A8; then a in the carrier of subrelstr B & b in the carrier of subrelstr B by YELLOW_0:def 15; then reconsider a1 = a, b1 = b as Element of subrelstr B ; A14: a1 <= a1 "\/" b1 & b1 <= a1 "\/" b1 by YELLOW_0:22; A15: sup {a,b} in B by A8,A12,A13,Th16; now per cases by A13,XBOOLE_0:def 2; suppose a in B \ J & b in B \ J; then A16: not a in J by XBOOLE_0:def 4; not a "\/" b in J proof assume a "\/" b in J; then a1 "\/" b1 in J1 by A9,YELLOW_0:71; hence contradiction by A14,A16,WAYBEL_0:def 19; end; then not sup {a,b} in J by YELLOW_0:41; then sup {a,b} in B \ J by A15,XBOOLE_0:def 4; hence sup {a,b} in C by XBOOLE_0:def 2; suppose a in B \ J & b in waybelow x /\ B; then A17: not a in J by XBOOLE_0:def 4; not a "\/" b in J proof assume a "\/" b in J; then a1 "\/" b1 in J1 by A9,YELLOW_0:71; hence contradiction by A14,A17,WAYBEL_0:def 19; end; then not sup {a,b} in J by YELLOW_0:41; then sup {a,b} in B \ J by A15,XBOOLE_0:def 4; hence sup {a,b} in C by XBOOLE_0:def 2; suppose a in waybelow x /\ B & b in B \ J; then A18: not b in J by XBOOLE_0:def 4; not a "\/" b in J proof assume a "\/" b in J; then a1 "\/" b1 in J1 by A9,YELLOW_0:71; hence contradiction by A14,A18,WAYBEL_0:def 19; end; then not sup {a,b} in J by YELLOW_0:41; then sup {a,b} in B \ J by A15,XBOOLE_0:def 4; hence sup {a,b} in C by XBOOLE_0:def 2; suppose a in waybelow x /\ B & b in waybelow x /\ B; then a in waybelow x & b in waybelow x by XBOOLE_0:def 3; then a << x & b << x by WAYBEL_3:7; then a "\/" b << x by WAYBEL_3:3; then a "\/" b in waybelow x by WAYBEL_3:7; then sup {a,b} in waybelow x by YELLOW_0:41; then sup {a,b} in waybelow x /\ B by A15,XBOOLE_0:def 3; hence sup {a,b} in C by XBOOLE_0:def 2; end; hence sup {a,b} in the carrier of subrelstr C by YELLOW_0:def 15; end; then A19: C is join-closed by Def2; now let y be Element of L; per cases; suppose not y <= x; then consider u be Element of L such that A20: u in B and A21: not u <= x and A22: u << y by Th46; A23: waybelow y /\ B is_<=_than sup(waybelow y /\ B) by YELLOW_0:32; A24: sup(waybelow y /\ B) is_>=_than waybelow y /\ C proof let b be Element of L; assume b in waybelow y /\ C; then b in waybelow y & b in C by XBOOLE_0:def 3; then b in waybelow y /\ B by A8,XBOOLE_0:def 3; hence b <= sup(waybelow y /\ B) by A23,LATTICE3:def 9; end; now let b be Element of L; assume A25: b is_>=_than waybelow y /\ C; b is_>=_than waybelow y /\ B proof let c be Element of L; assume c in waybelow y /\ B; then A26: c in waybelow y & c in B by XBOOLE_0:def 3; then c << y by WAYBEL_3:7; then c "\/" u << y by A22,WAYBEL_3:3; then A27: c "\/" u in waybelow y by WAYBEL_3:7; sup {c,u} in B by A20,A26,Th18; then A28: c "\/" u in B by YELLOW_0:41; A29: J is_<=_than x by YELLOW_0:32; u <= c "\/" u by YELLOW_0:22; then not c "\/" u <= x by A21,YELLOW_0:def 2; then not c "\/" u in J by A29,LATTICE3:def 9; then c "\/" u in B \ J by A28,XBOOLE_0:def 4; then c "\/" u in C by XBOOLE_0:def 2; then c "\/" u in waybelow y /\ C by A27,XBOOLE_0:def 3; then A30: c "\/" u <= b by A25,LATTICE3:def 9; c <= c "\/" u by YELLOW_0:22; hence c <= b by A30,YELLOW_0:def 2; end; hence sup(waybelow y /\ B) <= b by YELLOW_0:32; end; then sup(waybelow y /\ B) = sup(waybelow y /\ C) by A24,YELLOW_0:32; hence y = sup(waybelow y /\ C) by Def7; suppose A31: y <= x; A32: waybelow y /\ C c= waybelow y /\ B by A8,XBOOLE_1:26; waybelow y /\ B c= waybelow y /\ C proof let a be set; assume A33: a in waybelow y /\ B; then A34: a in waybelow y & a in B by XBOOLE_0:def 3; reconsider a1 = a as Element of L by A33; a1 << y by A34,WAYBEL_3:7; then a1 << x by A31,WAYBEL_3:2; then a1 in waybelow x by WAYBEL_3:7; then a in waybelow x /\ B by A34,XBOOLE_0:def 3; then a in C by XBOOLE_0:def 2; hence a in waybelow y /\ C by A34,XBOOLE_0:def 3; end; then waybelow y /\ B = waybelow y /\ C by A32,XBOOLE_0:def 10; hence y = sup(waybelow y /\ C) by Def7; end; then reconsider C as CLbasis of L by A19,Def7; A35: Bottom L in B by Def8; Bottom L << x by WAYBEL_3:4; then Bottom L in waybelow x by WAYBEL_3:7; then Bottom L in waybelow x /\ B by A35,XBOOLE_0:def 3; then Bottom L in C by XBOOLE_0:def 2; then C is with_bottom by Def8; then B c= C by A1; then A36: B = C by A8,XBOOLE_0:def 10; J c= waybelow x /\ B proof let a be set; assume A37: a in J; then a in J1; then a in the carrier of subrelstr B; then A38: a in C by A36,YELLOW_0:def 15; not a in B \ J2 by A37,XBOOLE_0:def 4; hence a in waybelow x /\ B by A38,XBOOLE_0:def 2; end; hence J = waybelow "\/"(J,L) /\ B by A2,XBOOLE_0:def 10; end; Lm5: for L be continuous lower-bounded LATTICE holds (ex B be with_bottom CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1) implies L is algebraic proof let L be continuous lower-bounded LATTICE; given B be with_bottom CLbasis of L such that A1: for B1 be with_bottom CLbasis of L holds B c= B1; A2: [supMap subrelstr B,baseMap B] is Galois by Th63; A3: rng supMap subrelstr B = the carrier of L by Th65; the carrier of InclPoset Ids subrelstr B c= rng baseMap B proof let J be set; assume J in the carrier of InclPoset Ids subrelstr B; then A4: J is Element of InclPoset Ids subrelstr B; set x = "\/"(J,L); J = waybelow x /\ B by A1,A4,Th71; then A5: J = (baseMap B).x by Def12; dom baseMap B = the carrier of L by FUNCT_2:def 1; hence J in rng baseMap B by A5,FUNCT_1:def 5; end; then rng baseMap B = the carrier of InclPoset Ids subrelstr B by XBOOLE_0:def 10 ; then baseMap B is onto by FUNCT_2:def 3; then A6: supMap subrelstr B is one-to-one by A2,WAYBEL_1:29; for x,y be Element of InclPoset Ids subrelstr B holds x <= y iff (supMap subrelstr B).x <= (supMap subrelstr B).y proof let x,y be Element of InclPoset Ids subrelstr B; thus x <= y implies (supMap subrelstr B).x <= (supMap subrelstr B).y by WAYBEL_1:def 2; reconsider x1 = x, y1 = y as Ideal of subrelstr B by YELLOW_2:43; A7: (supMap subrelstr B).x1 = "\/"(x1,L) & (supMap subrelstr B).y1 = "\/"(y1,L) by Def10; A8: x = waybelow "\/"(x,L) /\ B & y = waybelow "\/"(y,L) /\ B by A1,Th71; assume (supMap subrelstr B).x <= (supMap subrelstr B).y; then waybelow "\/"(x1,L) c= waybelow "\/"(y1,L) by A7,WAYBEL_3:25; then waybelow "\/"(x1,L) /\ B c= waybelow "\/"(y1,L) /\ B by XBOOLE_1:26; hence x <= y by A8,YELLOW_1:3; end; then supMap subrelstr B is isomorphic by A3,A6,WAYBEL_0:66; then A9: InclPoset Ids subrelstr B,L are_isomorphic by WAYBEL_1:def 8; InclPoset Ids subrelstr B is lower-bounded algebraic by WAYBEL13:10; hence L is algebraic by A9,WAYBEL13:32; end; theorem :: PROPOSITION 4.4. (1) iff (2) for L be continuous lower-bounded LATTICE holds L is algebraic iff the carrier of CompactSublatt L is with_bottom CLbasis of L & for B be with_bottom CLbasis of L holds the carrier of CompactSublatt L c= B by Lm4,Lm5; theorem :: PROPOSITION 4.4. (1) iff (3) for L be continuous lower-bounded LATTICE holds L is algebraic iff ex B be with_bottom CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1 proof let L be continuous lower-bounded LATTICE; thus L is algebraic implies ex B be with_bottom CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1 proof assume L is algebraic; then the carrier of CompactSublatt L is with_bottom CLbasis of L & for B be with_bottom CLbasis of L holds the carrier of CompactSublatt L c= B by Lm4; hence ex B be with_bottom CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1; end; thus (ex B be with_bottom CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1) implies L is algebraic by Lm5; end;

Back to top