:: WAYBEL_6 semantic presentation begin scheme :: WAYBEL_6:sch 1 NonUniqExD1{ F1() -> non empty RelStr , F2() -> Subset of F1(), F3() -> non empty Subset of F1(), P1[ set , set ] } : ex f being Function of F2(),F3() st for e being Element of F1() st e in F2() holds ex u being Element of F1() st ( u in F3() & u = f . e & P1[e,u] ) provided A1: for e being Element of F1() st e in F2() holds ex u being Element of F1() st ( u in F3() & P1[e,u] ) proof A2: for e being set st e in F2() holds ex u being set st ( u in F3() & P1[e,u] ) proof let e be set ; ::_thesis: ( e in F2() implies ex u being set st ( u in F3() & P1[e,u] ) ) assume A3: e in F2() ; ::_thesis: ex u being set st ( u in F3() & P1[e,u] ) then reconsider e1 = e as Element of F2() ; reconsider e1 = e1 as Element of F1() by A3; consider u being Element of F1() such that A4: ( u in F3() & P1[e1,u] ) by A1, A3; reconsider u1 = u as set ; take u1 ; ::_thesis: ( u1 in F3() & P1[e,u1] ) thus ( u1 in F3() & P1[e,u1] ) by A4; ::_thesis: verum end; consider f being Function such that A5: ( dom f = F2() & rng f c= F3() ) and A6: for e being set st e in F2() holds P1[e,f . e] from FUNCT_1:sch_5(A2); reconsider f = f as Function of F2(),F3() by A5, FUNCT_2:def_1, RELSET_1:4; take f ; ::_thesis: for e being Element of F1() st e in F2() holds ex u being Element of F1() st ( u in F3() & u = f . e & P1[e,u] ) for e being Element of F1() st e in F2() holds ex u being Element of F1() st ( u in F3() & u = f . e & P1[e,u] ) proof let e be Element of F1(); ::_thesis: ( e in F2() implies ex u being Element of F1() st ( u in F3() & u = f . e & P1[e,u] ) ) assume A7: e in F2() ; ::_thesis: ex u being Element of F1() st ( u in F3() & u = f . e & P1[e,u] ) then reconsider e1 = f . e as Element of F3() by FUNCT_2:5; reconsider fe = e1 as Element of F1() ; take fe ; ::_thesis: ( fe in F3() & fe = f . e & P1[e,fe] ) thus ( fe in F3() & fe = f . e & P1[e,fe] ) by A6, A7; ::_thesis: verum end; hence for e being Element of F1() st e in F2() holds ex u being Element of F1() st ( u in F3() & u = f . e & P1[e,u] ) ; ::_thesis: verum end; definition let L be LATTICE; let A be non empty Subset of L; let f be Function of A,A; let n be Element of NAT ; :: original: iter redefine func iter (f,n) -> Function of A,A; coherence iter (f,n) is Function of A,A by FUNCT_7:83; end; definition let L be LATTICE; let C, D be non empty Subset of L; let f be Function of C,D; let c be Element of C; :: original: . redefine funcf . c -> Element of L; coherence f . c is Element of L proof f . c in D ; hence f . c is Element of L ; ::_thesis: verum end; end; registration let L be non empty Poset; cluster strongly_connected -> directed filtered for Element of bool the carrier of L; coherence for b1 being Chain of L holds ( b1 is filtered & b1 is directed ) proof let C be Chain of L; ::_thesis: ( C is filtered & C is directed ) A1: the InternalRel of L is_strongly_connected_in C by ORDERS_2:def_7; thus C is filtered ::_thesis: C is directed proof let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in C or not y in C or ex b1 being Element of the carrier of L st ( b1 in C & b1 <= x & b1 <= y ) ) A2: ( x <= x & y <= y ) ; assume A3: ( x in C & y in C ) ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in C & b1 <= x & b1 <= y ) then ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A1, RELAT_2:def_7; then ( x <= y or y <= x ) by ORDERS_2:def_5; hence ex b1 being Element of the carrier of L st ( b1 in C & b1 <= x & b1 <= y ) by A3, A2; ::_thesis: verum end; let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in C or not y in C or ex b1 being Element of the carrier of L st ( b1 in C & x <= b1 & y <= b1 ) ) A4: ( x <= x & y <= y ) ; assume A5: ( x in C & y in C ) ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in C & x <= b1 & y <= b1 ) then ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A1, RELAT_2:def_7; then ( x <= y or y <= x ) by ORDERS_2:def_5; hence ex b1 being Element of the carrier of L st ( b1 in C & x <= b1 & y <= b1 ) by A5, A4; ::_thesis: verum end; end; registration cluster non empty strict V110() reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima continuous for RelStr ; existence ex b1 being LATTICE st ( b1 is strict & b1 is continuous & b1 is distributive & b1 is lower-bounded ) proof set x1 = the set ; set R = the Order of { the set }; reconsider RS = RelStr(# { the set }, the Order of { the set } #) as 1 -element reflexive RelStr ; take RS ; ::_thesis: ( RS is strict & RS is continuous & RS is distributive & RS is lower-bounded ) thus ( RS is strict & RS is continuous & RS is distributive & RS is lower-bounded ) ; ::_thesis: verum end; end; theorem Th1: :: WAYBEL_6:1 for S, T being Semilattice for f being Function of S,T holds ( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) proof let S, T be Semilattice; ::_thesis: for f being Function of S,T holds ( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) let f be Function of S,T; ::_thesis: ( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) A1: dom f = the carrier of S by FUNCT_2:def_1; thus ( f is meet-preserving implies for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) ::_thesis: ( ( for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) implies f is meet-preserving ) proof assume A2: f is meet-preserving ; ::_thesis: for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) let z, y be Element of S; ::_thesis: f . (z "/\" y) = (f . z) "/\" (f . y) A3: f preserves_inf_of {z,y} by A2, WAYBEL_0:def_34; A4: ( f .: {z,y} = {(f . z),(f . y)} & ex_inf_of {z,y},S ) by A1, FUNCT_1:60, YELLOW_0:21; thus f . (z "/\" y) = f . (inf {z,y}) by YELLOW_0:40 .= inf {(f . z),(f . y)} by A4, A3, WAYBEL_0:def_30 .= (f . z) "/\" (f . y) by YELLOW_0:40 ; ::_thesis: verum end; assume A5: for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ; ::_thesis: f is meet-preserving for z, y being Element of S holds f preserves_inf_of {z,y} proof let z, y be Element of S; ::_thesis: f preserves_inf_of {z,y} A6: f .: {z,y} = {(f . z),(f . y)} by A1, FUNCT_1:60; then A7: ( ex_inf_of {z,y},S implies ex_inf_of f .: {z,y},T ) by YELLOW_0:21; inf (f .: {z,y}) = (f . z) "/\" (f . y) by A6, YELLOW_0:40 .= f . (z "/\" y) by A5 .= f . (inf {z,y}) by YELLOW_0:40 ; hence f preserves_inf_of {z,y} by A7, WAYBEL_0:def_30; ::_thesis: verum end; hence f is meet-preserving by WAYBEL_0:def_34; ::_thesis: verum end; theorem Th2: :: WAYBEL_6:2 for S, T being sup-Semilattice for f being Function of S,T holds ( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) proof let S, T be sup-Semilattice; ::_thesis: for f being Function of S,T holds ( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) let f be Function of S,T; ::_thesis: ( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) A1: dom f = the carrier of S by FUNCT_2:def_1; thus ( f is join-preserving implies for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) ::_thesis: ( ( for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) implies f is join-preserving ) proof assume A2: f is join-preserving ; ::_thesis: for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) let z, y be Element of S; ::_thesis: f . (z "\/" y) = (f . z) "\/" (f . y) A3: f preserves_sup_of {z,y} by A2, WAYBEL_0:def_35; A4: ( f .: {z,y} = {(f . z),(f . y)} & ex_sup_of {z,y},S ) by A1, FUNCT_1:60, YELLOW_0:20; thus f . (z "\/" y) = f . (sup {z,y}) by YELLOW_0:41 .= sup {(f . z),(f . y)} by A4, A3, WAYBEL_0:def_31 .= (f . z) "\/" (f . y) by YELLOW_0:41 ; ::_thesis: verum end; assume A5: for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ; ::_thesis: f is join-preserving for z, y being Element of S holds f preserves_sup_of {z,y} proof let z, y be Element of S; ::_thesis: f preserves_sup_of {z,y} A6: f .: {z,y} = {(f . z),(f . y)} by A1, FUNCT_1:60; then A7: ( ex_sup_of {z,y},S implies ex_sup_of f .: {z,y},T ) by YELLOW_0:20; sup (f .: {z,y}) = (f . z) "\/" (f . y) by A6, YELLOW_0:41 .= f . (z "\/" y) by A5 .= f . (sup {z,y}) by YELLOW_0:41 ; hence f preserves_sup_of {z,y} by A7, WAYBEL_0:def_31; ::_thesis: verum end; hence f is join-preserving by WAYBEL_0:def_35; ::_thesis: verum end; theorem Th3: :: WAYBEL_6:3 for S, T being LATTICE for f being Function of S,T st T is distributive & f is meet-preserving & f is join-preserving & f is V24() holds S is distributive proof let S, T be LATTICE; ::_thesis: for f being Function of S,T st T is distributive & f is meet-preserving & f is join-preserving & f is V24() holds S is distributive let f be Function of S,T; ::_thesis: ( T is distributive & f is meet-preserving & f is join-preserving & f is V24() implies S is distributive ) assume that A1: T is distributive and A2: ( f is meet-preserving & f is join-preserving & f is V24() ) ; ::_thesis: S is distributive let x, y, z be Element of S; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) f . (x "/\" (y "\/" z)) = (f . x) "/\" (f . (y "\/" z)) by A2, Th1 .= (f . x) "/\" ((f . y) "\/" (f . z)) by A2, Th2 .= ((f . x) "/\" (f . y)) "\/" ((f . x) "/\" (f . z)) by A1, WAYBEL_1:def_3 .= ((f . x) "/\" (f . y)) "\/" (f . (x "/\" z)) by A2, Th1 .= (f . (x "/\" y)) "\/" (f . (x "/\" z)) by A2, Th1 .= f . ((x "/\" y) "\/" (x "/\" z)) by A2, Th2 ; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A2, FUNCT_2:19; ::_thesis: verum end; registration let S, T be complete LATTICE; cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like V32( the carrier of S, the carrier of T) sups-preserving for Element of bool [: the carrier of S, the carrier of T:]; existence ex b1 being Function of S,T st b1 is sups-preserving proof set t = Bottom T; set f = S --> (Bottom T); take S --> (Bottom T) ; ::_thesis: S --> (Bottom T) is sups-preserving let X be Subset of S; :: according to WAYBEL_0:def_33 ::_thesis: S --> (Bottom T) preserves_sup_of X assume ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (S --> (Bottom T)) .: X,T & "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S)) ) thus ex_sup_of (S --> (Bottom T)) .: X,T by YELLOW_0:17; ::_thesis: "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S)) ( (S --> (Bottom T)) .: X c= rng (S --> (Bottom T)) & rng (S --> (Bottom T)) c= {(Bottom T)} ) by FUNCOP_1:13, RELAT_1:111; then (S --> (Bottom T)) .: X c= {(Bottom T)} by XBOOLE_1:1; then A1: ( (S --> (Bottom T)) .: X = {(Bottom T)} or (S --> (Bottom T)) .: X = {} ) by ZFMISC_1:33; percases ( X = {} or X <> {} ) ; suppose X = {} ; ::_thesis: "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S)) then (S --> (Bottom T)) .: X = {} ; then sup ((S --> (Bottom T)) .: X) = Bottom T by YELLOW_0:def_11; hence "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S)) by FUNCOP_1:7; ::_thesis: verum end; suppose X <> {} ; ::_thesis: "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S)) then reconsider X1 = X as non empty Subset of S ; set x = the Element of X1; (S --> (Bottom T)) . the Element of X1 in (S --> (Bottom T)) .: X by FUNCT_2:35; hence sup ((S --> (Bottom T)) .: X) = Bottom T by A1, YELLOW_0:39 .= (S --> (Bottom T)) . (sup X) by FUNCOP_1:7 ; ::_thesis: verum end; end; end; end; Lm1: for S, T being non empty with_suprema Poset for f being Function of S,T st f is directed-sups-preserving holds f is monotone proof let S, T be non empty with_suprema Poset; ::_thesis: for f being Function of S,T st f is directed-sups-preserving holds f is monotone let f be Function of S,T; ::_thesis: ( f is directed-sups-preserving implies f is monotone ) assume A1: f is directed-sups-preserving ; ::_thesis: f is monotone let x, y be Element of S; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) ) assume A2: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) A3: y = y "\/" x by A2, YELLOW_0:24; for a, b being Element of S st a in {x,y} & b in {x,y} holds ex z being Element of S st ( z in {x,y} & a <= z & b <= z ) proof let a, b be Element of S; ::_thesis: ( a in {x,y} & b in {x,y} implies ex z being Element of S st ( z in {x,y} & a <= z & b <= z ) ) assume A4: ( a in {x,y} & b in {x,y} ) ; ::_thesis: ex z being Element of S st ( z in {x,y} & a <= z & b <= z ) take y ; ::_thesis: ( y in {x,y} & a <= y & b <= y ) thus y in {x,y} by TARSKI:def_2; ::_thesis: ( a <= y & b <= y ) thus ( a <= y & b <= y ) by A2, A4, TARSKI:def_2; ::_thesis: verum end; then ( {x,y} is directed & not {x,y} is empty ) by WAYBEL_0:def_1; then A5: f preserves_sup_of {x,y} by A1, WAYBEL_0:def_37; A6: dom f = the carrier of S by FUNCT_2:def_1; y <= y ; then A7: {x,y} is_<=_than y by A2, YELLOW_0:8; for b being Element of S st {x,y} is_<=_than b holds y <= b by YELLOW_0:8; then ex_sup_of {x,y},S by A7, YELLOW_0:30; then sup (f .: {x,y}) = f . (sup {x,y}) by A5, WAYBEL_0:def_31 .= f . y by A3, YELLOW_0:41 ; then A8: f . y = sup {(f . x),(f . y)} by A6, FUNCT_1:60 .= (f . y) "\/" (f . x) by YELLOW_0:41 ; let afx, bfy be Element of T; ::_thesis: ( not afx = f . x or not bfy = f . y or afx <= bfy ) assume ( afx = f . x & bfy = f . y ) ; ::_thesis: afx <= bfy hence afx <= bfy by A8, YELLOW_0:22; ::_thesis: verum end; theorem Th4: :: WAYBEL_6:4 for S, T being complete LATTICE for f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving & f is V24() holds S is meet-continuous proof let S, T be complete LATTICE; ::_thesis: for f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving & f is V24() holds S is meet-continuous let f be sups-preserving Function of S,T; ::_thesis: ( T is meet-continuous & f is meet-preserving & f is V24() implies S is meet-continuous ) assume that A1: T is meet-continuous and A2: ( f is meet-preserving & f is V24() ) ; ::_thesis: S is meet-continuous S is satisfying_MC proof let x be Element of S; :: according to WAYBEL_2:def_6 ::_thesis: for b1 being Element of bool the carrier of S holds x "/\" ("\/" (b1,S)) = "\/" (({x} "/\" b1),S) let D be non empty directed Subset of S; ::_thesis: x "/\" ("\/" (D,S)) = "\/" (({x} "/\" D),S) A3: ( ex_sup_of D,S & f preserves_sup_of D ) by WAYBEL_0:75, WAYBEL_0:def_33; reconsider Y = {x} as non empty directed Subset of S by WAYBEL_0:5; A4: ( ex_sup_of Y "/\" D,S & f preserves_sup_of {x} "/\" D ) by WAYBEL_0:75, WAYBEL_0:def_33; reconsider X = f .: D as directed Subset of T by Lm1, YELLOW_2:15; A5: dom f = the carrier of S by FUNCT_2:def_1; A6: {(f . x)} "/\" (f .: D) = { ((f . x) "/\" y) where y is Element of T : y in f .: D } by YELLOW_4:42; A7: {(f . x)} "/\" (f .: D) c= f .: ({x} "/\" D) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in {(f . x)} "/\" (f .: D) or p in f .: ({x} "/\" D) ) assume p in {(f . x)} "/\" (f .: D) ; ::_thesis: p in f .: ({x} "/\" D) then consider y being Element of T such that A8: p = (f . x) "/\" y and A9: y in f .: D by A6; consider k being set such that A10: k in dom f and A11: k in D and A12: y = f . k by A9, FUNCT_1:def_6; reconsider k = k as Element of S by A10; x "/\" k in { (x "/\" a) where a is Element of S : a in D } by A11; then A13: x "/\" k in {x} "/\" D by YELLOW_4:42; f preserves_inf_of {x,k} by A2, WAYBEL_0:def_34; then p = f . (x "/\" k) by A8, A12, YELLOW_3:8; hence p in f .: ({x} "/\" D) by A5, A13, FUNCT_1:def_6; ::_thesis: verum end; A14: {x} "/\" D = { (x "/\" y) where y is Element of S : y in D } by YELLOW_4:42; A15: f .: ({x} "/\" D) c= {(f . x)} "/\" (f .: D) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in f .: ({x} "/\" D) or p in {(f . x)} "/\" (f .: D) ) assume p in f .: ({x} "/\" D) ; ::_thesis: p in {(f . x)} "/\" (f .: D) then consider m being set such that A16: m in dom f and A17: m in {x} "/\" D and A18: p = f . m by FUNCT_1:def_6; reconsider m = m as Element of S by A16; consider a being Element of S such that A19: m = x "/\" a and A20: a in D by A14, A17; reconsider fa = f . a as Element of T ; f preserves_inf_of {x,a} by A2, WAYBEL_0:def_34; then A21: p = (f . x) "/\" fa by A18, A19, YELLOW_3:8; fa in f .: D by A5, A20, FUNCT_1:def_6; hence p in {(f . x)} "/\" (f .: D) by A6, A21; ::_thesis: verum end; f . (x "/\" (sup D)) = (f . x) "/\" (f . (sup D)) by A2, Th1 .= (f . x) "/\" (sup X) by A3, WAYBEL_0:def_31 .= sup ({(f . x)} "/\" X) by A1, WAYBEL_2:def_6 .= sup (f .: ({x} "/\" D)) by A7, A15, XBOOLE_0:def_10 .= f . (sup ({x} "/\" D)) by A4, WAYBEL_0:def_31 ; hence x "/\" (sup D) = sup ({x} "/\" D) by A2, A5, FUNCT_1:def_4; ::_thesis: verum end; hence S is meet-continuous ; ::_thesis: verum end; begin definition let L be non empty reflexive RelStr ; let X be Subset of L; attrX is Open means :Def1: :: WAYBEL_6:def 1 for x being Element of L st x in X holds ex y being Element of L st ( y in X & y << x ); end; :: deftheorem Def1 defines Open WAYBEL_6:def_1_:_ for L being non empty reflexive RelStr for X being Subset of L holds ( X is Open iff for x being Element of L st x in X holds ex y being Element of L st ( y in X & y << x ) ); theorem :: WAYBEL_6:5 for L being up-complete LATTICE for X being upper Subset of L holds ( X is Open iff for x being Element of L st x in X holds waybelow x meets X ) proof let L be up-complete LATTICE; ::_thesis: for X being upper Subset of L holds ( X is Open iff for x being Element of L st x in X holds waybelow x meets X ) let X be upper Subset of L; ::_thesis: ( X is Open iff for x being Element of L st x in X holds waybelow x meets X ) hereby ::_thesis: ( ( for x being Element of L st x in X holds waybelow x meets X ) implies X is Open ) assume A1: X is Open ; ::_thesis: for x being Element of L st x in X holds waybelow x meets X thus for x being Element of L st x in X holds waybelow x meets X ::_thesis: verum proof let x be Element of L; ::_thesis: ( x in X implies waybelow x meets X ) assume x in X ; ::_thesis: waybelow x meets X then consider y being Element of L such that A2: y in X and A3: y << x by A1, Def1; y in { y1 where y1 is Element of L : y1 << x } by A3; then y in waybelow x by WAYBEL_3:def_3; hence waybelow x meets X by A2, XBOOLE_0:3; ::_thesis: verum end; end; assume A4: for x being Element of L st x in X holds waybelow x meets X ; ::_thesis: X is Open now__::_thesis:_for_x1_being_Element_of_L_st_x1_in_X_holds_ ex_z_being_Element_of_L_st_ (_z_in_X_&_z_<<_x1_) let x1 be Element of L; ::_thesis: ( x1 in X implies ex z being Element of L st ( z in X & z << x1 ) ) assume x1 in X ; ::_thesis: ex z being Element of L st ( z in X & z << x1 ) then waybelow x1 meets X by A4; then consider y being set such that A5: y in waybelow x1 and A6: y in X by XBOOLE_0:3; waybelow x1 = { y1 where y1 is Element of L : y1 << x1 } by WAYBEL_3:def_3; then ex z being Element of L st ( z = y & z << x1 ) by A5; hence ex z being Element of L st ( z in X & z << x1 ) by A6; ::_thesis: verum end; hence X is Open by Def1; ::_thesis: verum end; theorem :: WAYBEL_6:6 for L being up-complete LATTICE for X being upper Subset of L holds ( X is Open iff X = union { (wayabove x) where x is Element of L : x in X } ) proof let L be up-complete LATTICE; ::_thesis: for X being upper Subset of L holds ( X is Open iff X = union { (wayabove x) where x is Element of L : x in X } ) let X be upper Subset of L; ::_thesis: ( X is Open iff X = union { (wayabove x) where x is Element of L : x in X } ) hereby ::_thesis: ( X = union { (wayabove x) where x is Element of L : x in X } implies X is Open ) assume A1: X is Open ; ::_thesis: X = union { (wayabove x) where x is Element of L : x in X } A2: X c= union { (wayabove x) where x is Element of L : x in X } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X or z in union { (wayabove x) where x is Element of L : x in X } ) assume A3: z in X ; ::_thesis: z in union { (wayabove x) where x is Element of L : x in X } then reconsider x1 = z as Element of X ; reconsider x1 = x1 as Element of L by A3; consider y being Element of L such that A4: y in X and A5: y << x1 by A1, A3, Def1; x1 in { y1 where y1 is Element of L : y1 >> y } by A5; then A6: x1 in wayabove y by WAYBEL_3:def_4; wayabove y in { (wayabove x) where x is Element of L : x in X } by A4; hence z in union { (wayabove x) where x is Element of L : x in X } by A6, TARSKI:def_4; ::_thesis: verum end; union { (wayabove x) where x is Element of L : x in X } c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { (wayabove x) where x is Element of L : x in X } or z in X ) assume z in union { (wayabove x) where x is Element of L : x in X } ; ::_thesis: z in X then consider Y being set such that A7: z in Y and A8: Y in { (wayabove x) where x is Element of L : x in X } by TARSKI:def_4; consider x being Element of L such that A9: Y = wayabove x and A10: x in X by A8; z in { y where y is Element of L : y >> x } by A7, A9, WAYBEL_3:def_4; then consider z1 being Element of L such that A11: z1 = z and A12: z1 >> x ; x <= z1 by A12, WAYBEL_3:1; hence z in X by A10, A11, WAYBEL_0:def_20; ::_thesis: verum end; hence X = union { (wayabove x) where x is Element of L : x in X } by A2, XBOOLE_0:def_10; ::_thesis: verum end; assume A13: X = union { (wayabove x) where x is Element of L : x in X } ; ::_thesis: X is Open now__::_thesis:_for_x1_being_Element_of_L_st_x1_in_X_holds_ ex_x_being_Element_of_L_st_ (_x_in_X_&_x_<<_x1_) let x1 be Element of L; ::_thesis: ( x1 in X implies ex x being Element of L st ( x in X & x << x1 ) ) assume x1 in X ; ::_thesis: ex x being Element of L st ( x in X & x << x1 ) then consider Y being set such that A14: x1 in Y and A15: Y in { (wayabove x) where x is Element of L : x in X } by A13, TARSKI:def_4; consider x being Element of L such that A16: Y = wayabove x and A17: x in X by A15; x1 in { y where y is Element of L : y >> x } by A14, A16, WAYBEL_3:def_4; then ex z1 being Element of L st ( z1 = x1 & z1 >> x ) ; hence ex x being Element of L st ( x in X & x << x1 ) by A17; ::_thesis: verum end; hence X is Open by Def1; ::_thesis: verum end; registration let L be lower-bounded up-complete LATTICE; cluster non empty filtered upper Open for Element of bool the carrier of L; existence ex b1 being Filter of L st b1 is Open proof take [#] L ; ::_thesis: [#] L is Open now__::_thesis:_for_x_being_Element_of_L_st_x_in_[#]_L_holds_ ex_y_being_Element_of_L_st_ (_y_in_[#]_L_&_y_<<_x_) let x be Element of L; ::_thesis: ( x in [#] L implies ex y being Element of L st ( y in [#] L & y << x ) ) assume x in [#] L ; ::_thesis: ex y being Element of L st ( y in [#] L & y << x ) Bottom L << x by WAYBEL_3:4; hence ex y being Element of L st ( y in [#] L & y << x ) ; ::_thesis: verum end; hence [#] L is Open by Def1; ::_thesis: verum end; end; theorem :: WAYBEL_6:7 for L being lower-bounded continuous LATTICE for x being Element of L holds wayabove x is Open proof let L be lower-bounded continuous LATTICE; ::_thesis: for x being Element of L holds wayabove x is Open let x be Element of L; ::_thesis: wayabove x is Open for l being Element of L st l in wayabove x holds ex y being Element of L st ( y in wayabove x & y << l ) proof let l be Element of L; ::_thesis: ( l in wayabove x implies ex y being Element of L st ( y in wayabove x & y << l ) ) assume l in wayabove x ; ::_thesis: ex y being Element of L st ( y in wayabove x & y << l ) then x << l by WAYBEL_3:8; then consider y being Element of L such that A1: ( x << y & y << l ) by WAYBEL_4:52; take y ; ::_thesis: ( y in wayabove x & y << l ) thus ( y in wayabove x & y << l ) by A1, WAYBEL_3:8; ::_thesis: verum end; hence wayabove x is Open by Def1; ::_thesis: verum end; theorem Th8: :: WAYBEL_6:8 for L being lower-bounded continuous LATTICE for x, y being Element of L st x << y holds ex F being Open Filter of L st ( y in F & F c= wayabove x ) proof let L be lower-bounded continuous LATTICE; ::_thesis: for x, y being Element of L st x << y holds ex F being Open Filter of L st ( y in F & F c= wayabove x ) let x, y be Element of L; ::_thesis: ( x << y implies ex F being Open Filter of L st ( y in F & F c= wayabove x ) ) defpred S1[ Element of L, Element of L] means $2 << $1; assume A1: x << y ; ::_thesis: ex F being Open Filter of L st ( y in F & F c= wayabove x ) then reconsider W = wayabove x as non empty Subset of L by WAYBEL_3:8; A2: for z being Element of L st z in W holds ex z1 being Element of L st ( z1 in W & S1[z,z1] ) proof let z be Element of L; ::_thesis: ( z in W implies ex z1 being Element of L st ( z1 in W & S1[z,z1] ) ) assume z in W ; ::_thesis: ex z1 being Element of L st ( z1 in W & S1[z,z1] ) then x << z by WAYBEL_3:8; then consider x9 being Element of L such that A3: x << x9 and A4: x9 << z by WAYBEL_4:52; x9 in W by A3, WAYBEL_3:8; hence ex z1 being Element of L st ( z1 in W & S1[z,z1] ) by A4; ::_thesis: verum end; consider f being Function of W,W such that A5: for z being Element of L st z in W holds ex z1 being Element of L st ( z1 in W & z1 = f . z & S1[z,z1] ) from WAYBEL_6:sch_1(A2); set V = { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ; now__::_thesis:_for_u1_being_set_st_u1_in__{__(uparrow_z)_where_z_is_Element_of_L_:_ex_n_being_Element_of_NAT_st_z_=_(iter_(f,n))_._y__}__holds_ u1_in_bool_the_carrier_of_L let u1 be set ; ::_thesis: ( u1 in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } implies u1 in bool the carrier of L ) assume u1 in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ; ::_thesis: u1 in bool the carrier of L then ex z being Element of L st ( u1 = uparrow z & ex n being Element of NAT st z = (iter (f,n)) . y ) ; hence u1 in bool the carrier of L ; ::_thesis: verum end; then reconsider V = { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } as Subset-Family of L by TARSKI:def_3; A6: for X, Y being Subset of L st X in V & Y in V holds ex Z being Subset of L st ( Z in V & X \/ Y c= Z ) proof reconsider y1 = y as Element of W by A1, WAYBEL_3:8; let X, Y be Subset of L; ::_thesis: ( X in V & Y in V implies ex Z being Subset of L st ( Z in V & X \/ Y c= Z ) ) assume that A7: X in V and A8: Y in V ; ::_thesis: ex Z being Subset of L st ( Z in V & X \/ Y c= Z ) consider z2 being Element of L such that A9: Y = uparrow z2 and A10: ex n being Element of NAT st z2 = (iter (f,n)) . y by A8; consider n2 being Element of NAT such that A11: z2 = (iter (f,n2)) . y by A10; consider z1 being Element of L such that A12: X = uparrow z1 and A13: ex n being Element of NAT st z1 = (iter (f,n)) . y by A7; set z = z1 "/\" z2; consider n1 being Element of NAT such that A14: z1 = (iter (f,n1)) . y by A13; A15: for n, k being Element of NAT holds (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1 proof let n be Element of NAT ; ::_thesis: for k being Element of NAT holds (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1 defpred S2[ Element of NAT ] means (iter (f,(n + $1))) . y1 <= (iter (f,n)) . y1; A16: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A17: (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1 ; ::_thesis: S2[k + 1] set nk = (iter (f,(n + k))) . y1; (iter (f,(n + k))) . y1 in W by FUNCT_2:5; then consider znk being Element of L such that znk in W and A18: znk = f . ((iter (f,(n + k))) . y1) and A19: znk << (iter (f,(n + k))) . y1 by A5; dom (iter (f,(n + k))) = W by FUNCT_2:def_1; then A20: znk = (f * (iter (f,(n + k)))) . y1 by A18, FUNCT_1:13 .= (iter (f,((n + k) + 1))) . y1 by FUNCT_7:71 .= (iter (f,(n + (k + 1)))) . y1 ; znk <= (iter (f,(n + k))) . y1 by A19, WAYBEL_3:1; hence S2[k + 1] by A17, A20, ORDERS_2:3; ::_thesis: verum end; A21: S2[ 0 ] ; for k being Element of NAT holds S2[k] from NAT_1:sch_1(A21, A16); hence for k being Element of NAT holds (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1 ; ::_thesis: verum end; A22: now__::_thesis:_uparrow_(z1_"/\"_z2)_in_V percases ( n1 <= n2 or n2 <= n1 ) ; suppose n1 <= n2 ; ::_thesis: uparrow (z1 "/\" z2) in V then consider k being Nat such that A23: n1 + k = n2 by NAT_1:10; k in NAT by ORDINAL1:def_12; then z2 <= z1 by A14, A11, A15, A23; hence uparrow (z1 "/\" z2) in V by A8, A9, YELLOW_0:25; ::_thesis: verum end; suppose n2 <= n1 ; ::_thesis: uparrow (z1 "/\" z2) in V then consider k being Nat such that A24: n2 + k = n1 by NAT_1:10; k in NAT by ORDINAL1:def_12; then z1 <= z2 by A14, A11, A15, A24; hence uparrow (z1 "/\" z2) in V by A7, A12, YELLOW_0:25; ::_thesis: verum end; end; end; z1 "/\" z2 <= z2 by YELLOW_0:23; then A25: uparrow z2 c= uparrow (z1 "/\" z2) by WAYBEL_0:22; z1 "/\" z2 <= z1 by YELLOW_0:23; then uparrow z1 c= uparrow (z1 "/\" z2) by WAYBEL_0:22; hence ex Z being Subset of L st ( Z in V & X \/ Y c= Z ) by A12, A9, A22, A25, XBOOLE_1:8; ::_thesis: verum end; A26: for X being Subset of L st X in V holds X is filtered proof let X be Subset of L; ::_thesis: ( X in V implies X is filtered ) assume X in V ; ::_thesis: X is filtered then ex z being Element of L st ( X = uparrow z & ex n being Element of NAT st z = (iter (f,n)) . y ) ; hence X is filtered ; ::_thesis: verum end; y <= y ; then A27: y in uparrow y by WAYBEL_0:18; set F = union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ; now__::_thesis:_for_u1_being_set_st_u1_in_union__{__(uparrow_z)_where_z_is_Element_of_L_:_ex_n_being_Element_of_NAT_st_z_=_(iter_(f,n))_._y__}__holds_ u1_in_the_carrier_of_L let u1 be set ; ::_thesis: ( u1 in union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } implies u1 in the carrier of L ) assume u1 in union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ; ::_thesis: u1 in the carrier of L then consider Y being set such that A28: u1 in Y and A29: Y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } by TARSKI:def_4; consider z being Element of L such that A30: Y = uparrow z and ex n being Element of NAT st z = (iter (f,n)) . y by A29; reconsider z1 = {z} as Subset of L ; u1 in { a where a is Element of L : ex b being Element of L st ( a >= b & b in z1 ) } by A28, A30, WAYBEL_0:15; then ex a being Element of L st ( a = u1 & ex b being Element of L st ( a >= b & b in z1 ) ) ; hence u1 in the carrier of L ; ::_thesis: verum end; then reconsider F = union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } as Subset of L by TARSKI:def_3; A31: y in wayabove x by A1, WAYBEL_3:8; A32: now__::_thesis:_for_u1_being_Element_of_L_st_u1_in_F_holds_ ex_g_being_Element_of_L_st_ (_g_in_F_&_g_<<_u1_) let u1 be Element of L; ::_thesis: ( u1 in F implies ex g being Element of L st ( g in F & g << u1 ) ) assume u1 in F ; ::_thesis: ex g being Element of L st ( g in F & g << u1 ) then consider Y being set such that A33: u1 in Y and A34: Y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } by TARSKI:def_4; consider z being Element of L such that A35: Y = uparrow z and A36: ex n being Element of NAT st z = (iter (f,n)) . y by A34; consider n being Element of NAT such that A37: z = (iter (f,n)) . y by A36; z in W by A31, A37, FUNCT_2:5; then consider z9 being Element of L such that z9 in W and A38: z9 = f . z and A39: z9 << z by A5; z9 <= z9 ; then A40: z9 in uparrow z9 by WAYBEL_0:18; dom (iter (f,n)) = W by FUNCT_2:def_1; then z9 = (f * (iter (f,n))) . y by A31, A37, A38, FUNCT_1:13 .= (iter (f,(n + 1))) . y by FUNCT_7:71 ; then uparrow z9 in { (uparrow p) where p is Element of L : ex n being Element of NAT st p = (iter (f,n)) . y } ; then A41: z9 in F by A40, TARSKI:def_4; reconsider z1 = {z} as Subset of L ; u1 in { a where a is Element of L : ex b being Element of L st ( a >= b & b in z1 ) } by A33, A35, WAYBEL_0:15; then consider a being Element of L such that A42: a = u1 and A43: ex b being Element of L st ( a >= b & b in z1 ) ; consider b being Element of L such that A44: a >= b and A45: b in z1 by A43; b = z by A45, TARSKI:def_1; hence ex g being Element of L st ( g in F & g << u1 ) by A42, A44, A39, A41, WAYBEL_3:2; ::_thesis: verum end; dom f = W by FUNCT_2:def_1; then A46: y in field f by A31, XBOOLE_0:def_3; (iter (f,0)) . y = (id (field f)) . y by FUNCT_7:68 .= y by A46, FUNCT_1:18 ; then A47: uparrow y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ; for X being Subset of L st X in V holds X is upper proof let X be Subset of L; ::_thesis: ( X in V implies X is upper ) assume X in V ; ::_thesis: X is upper then ex z being Element of L st ( X = uparrow z & ex n being Element of NAT st z = (iter (f,n)) . y ) ; hence X is upper ; ::_thesis: verum end; then reconsider F = F as Open Filter of L by A27, A47, A26, A6, A32, Def1, TARSKI:def_4, WAYBEL_0:28, WAYBEL_0:47; take F ; ::_thesis: ( y in F & F c= wayabove x ) now__::_thesis:_for_u1_being_set_st_u1_in_F_holds_ u1_in_wayabove_x let u1 be set ; ::_thesis: ( u1 in F implies u1 in wayabove x ) assume A48: u1 in F ; ::_thesis: u1 in wayabove x then consider Y being set such that A49: u1 in Y and A50: Y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } by TARSKI:def_4; reconsider u = u1 as Element of L by A48; consider z being Element of L such that A51: Y = uparrow z and A52: ex n being Element of NAT st z = (iter (f,n)) . y by A50; z in wayabove x by A31, A52, FUNCT_2:5; then A53: x << z by WAYBEL_3:8; z <= u by A49, A51, WAYBEL_0:18; then x << u by A53, WAYBEL_3:2; hence u1 in wayabove x by WAYBEL_3:8; ::_thesis: verum end; hence ( y in F & F c= wayabove x ) by A27, A47, TARSKI:def_3, TARSKI:def_4; ::_thesis: verum end; theorem Th9: :: WAYBEL_6:9 for L being complete LATTICE for X being upper Open Subset of L for x being Element of L st x in X ` holds ex m being Element of L st ( x <= m & m is_maximal_in X ` ) proof let L be complete LATTICE; ::_thesis: for X being upper Open Subset of L for x being Element of L st x in X ` holds ex m being Element of L st ( x <= m & m is_maximal_in X ` ) let X be upper Open Subset of L; ::_thesis: for x being Element of L st x in X ` holds ex m being Element of L st ( x <= m & m is_maximal_in X ` ) let x be Element of L; ::_thesis: ( x in X ` implies ex m being Element of L st ( x <= m & m is_maximal_in X ` ) ) set A = { C where C is Chain of L : ( C c= X ` & x in C ) } ; reconsider x1 = {x} as Chain of L by ORDERS_2:8; A1: for Z being set st Z <> {} & Z c= { C where C is Chain of L : ( C c= X ` & x in C ) } & Z is c=-linear holds union Z in { C where C is Chain of L : ( C c= X ` & x in C ) } proof let Z be set ; ::_thesis: ( Z <> {} & Z c= { C where C is Chain of L : ( C c= X ` & x in C ) } & Z is c=-linear implies union Z in { C where C is Chain of L : ( C c= X ` & x in C ) } ) assume that A2: Z <> {} and A3: Z c= { C where C is Chain of L : ( C c= X ` & x in C ) } and A4: Z is c=-linear ; ::_thesis: union Z in { C where C is Chain of L : ( C c= X ` & x in C ) } now__::_thesis:_for_Y_being_set_st_Y_in_Z_holds_ Y_c=_the_carrier_of_L let Y be set ; ::_thesis: ( Y in Z implies Y c= the carrier of L ) assume Y in Z ; ::_thesis: Y c= the carrier of L then Y in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3; then ex C being Chain of L st ( Y = C & C c= X ` & x in C ) ; hence Y c= the carrier of L ; ::_thesis: verum end; then reconsider UZ = union Z as Subset of L by ZFMISC_1:76; the InternalRel of L is_strongly_connected_in UZ proof let a, b be set ; :: according to RELAT_2:def_7 ::_thesis: ( not a in UZ or not b in UZ or [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) assume that A5: a in UZ and A6: b in UZ ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) consider az being set such that A7: a in az and A8: az in Z by A5, TARSKI:def_4; consider bz being set such that A9: b in bz and A10: bz in Z by A6, TARSKI:def_4; az,bz are_c=-comparable by A4, A8, A10, ORDINAL1:def_8; then A11: ( az c= bz or bz c= az ) by XBOOLE_0:def_9; bz in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3, A10; then A12: ex C being Chain of L st ( bz = C & C c= X ` & x in C ) ; az in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3, A8; then A13: ex C being Chain of L st ( az = C & C c= X ` & x in C ) ; reconsider bz = bz as Chain of L by A12; reconsider az = az as Chain of L by A13; ( the InternalRel of L is_strongly_connected_in az & the InternalRel of L is_strongly_connected_in bz ) by ORDERS_2:def_7; hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by A7, A9, A11, RELAT_2:def_7; ::_thesis: verum end; then reconsider UZ = UZ as Chain of L by ORDERS_2:def_7; A14: now__::_thesis:_for_Y_being_set_st_Y_in_Z_holds_ Y_c=_X_` let Y be set ; ::_thesis: ( Y in Z implies Y c= X ` ) assume Y in Z ; ::_thesis: Y c= X ` then Y in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3; then ex C being Chain of L st ( Y = C & C c= X ` & x in C ) ; hence Y c= X ` ; ::_thesis: verum end; set Y = the Element of Z; the Element of Z in Z by A2; then the Element of Z in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3; then ex C being Chain of L st ( the Element of Z = C & C c= X ` & x in C ) ; then A15: x in UZ by A2, TARSKI:def_4; UZ c= X ` by A14, ZFMISC_1:76; hence union Z in { C where C is Chain of L : ( C c= X ` & x in C ) } by A15; ::_thesis: verum end; assume x in X ` ; ::_thesis: ex m being Element of L st ( x <= m & m is_maximal_in X ` ) then A16: x1 c= X ` by ZFMISC_1:31; x in x1 by ZFMISC_1:31; then x1 in { C where C is Chain of L : ( C c= X ` & x in C ) } by A16; then consider Y1 being set such that A17: Y1 in { C where C is Chain of L : ( C c= X ` & x in C ) } and A18: for Z being set st Z in { C where C is Chain of L : ( C c= X ` & x in C ) } & Z <> Y1 holds not Y1 c= Z by A1, ORDERS_1:67; consider Y being Chain of L such that A19: Y = Y1 and A20: Y c= X ` and A21: x in Y by A17; set m = sup Y; sup Y is_>=_than Y by YELLOW_0:32; then A22: x <= sup Y by A21, LATTICE3:def_9; A23: sup Y is_>=_than Y by YELLOW_0:32; A24: now__::_thesis:_for_y_being_Element_of_L_holds_ (_not_y_in_X_`_or_not_y_>_sup_Y_) given y being Element of L such that A25: y in X ` and A26: y > sup Y ; ::_thesis: contradiction A27: now__::_thesis:_not_y_in_Y assume y in Y ; ::_thesis: contradiction then y <= sup Y by A23, LATTICE3:def_9; hence contradiction by A26, ORDERS_2:6; ::_thesis: verum end; set Y2 = Y \/ {y}; A28: sup Y <= y by A26, ORDERS_2:def_6; the InternalRel of L is_strongly_connected_in Y \/ {y} proof let a, b be set ; :: according to RELAT_2:def_7 ::_thesis: ( not a in Y \/ {y} or not b in Y \/ {y} or [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) assume A29: ( a in Y \/ {y} & b in Y \/ {y} ) ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) percases ( ( a in Y & b in Y ) or ( a in Y & b in {y} ) or ( a in {y} & b in Y ) or ( a in {y} & b in {y} ) ) by A29, XBOOLE_0:def_3; supposeA30: ( a in Y & b in Y ) ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) the InternalRel of L is_strongly_connected_in Y by ORDERS_2:def_7; hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by A30, RELAT_2:def_7; ::_thesis: verum end; supposeA31: ( a in Y & b in {y} ) ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) then reconsider a1 = a as Element of L ; reconsider b1 = b as Element of L by A31; ( b1 = y & a1 <= sup Y ) by A23, A31, LATTICE3:def_9, TARSKI:def_1; then a1 <= b1 by A28, ORDERS_2:3; hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum end; supposeA32: ( a in {y} & b in Y ) ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) then reconsider a1 = b as Element of L ; reconsider b1 = a as Element of L by A32; ( b1 = y & a1 <= sup Y ) by A23, A32, LATTICE3:def_9, TARSKI:def_1; then a1 <= b1 by A28, ORDERS_2:3; hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum end; supposeA33: ( a in {y} & b in {y} ) ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) then reconsider a1 = a as Element of L ; A34: a1 <= a1 ; ( a = y & b = y ) by A33, TARSKI:def_1; hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by A34, ORDERS_2:def_5; ::_thesis: verum end; end; end; then reconsider Y2 = Y \/ {y} as Chain of L by ORDERS_2:def_7; {y} c= X ` by A25, ZFMISC_1:31; then A35: Y2 c= X ` by A20, XBOOLE_1:8; y in {y} by TARSKI:def_1; then A36: y in Y2 by XBOOLE_0:def_3; x in Y2 by A21, XBOOLE_0:def_3; then Y2 in { C where C is Chain of L : ( C c= X ` & x in C ) } by A35; hence contradiction by A18, A19, A27, A36, XBOOLE_1:7; ::_thesis: verum end; now__::_thesis:_not_sup_Y_in_X assume sup Y in X ; ::_thesis: contradiction then consider y being Element of L such that A37: y in X and A38: y << sup Y by Def1; consider d being Element of L such that A39: d in Y and A40: y <= d by A21, A38, WAYBEL_3:def_1; d in X by A37, A40, WAYBEL_0:def_20; hence contradiction by A20, A39, XBOOLE_0:def_5; ::_thesis: verum end; then sup Y in X ` by XBOOLE_0:def_5; then sup Y is_maximal_in X ` by A24, WAYBEL_4:55; hence ex m being Element of L st ( x <= m & m is_maximal_in X ` ) by A22; ::_thesis: verum end; begin definition let G be non empty RelStr ; let g be Element of G; attrg is meet-irreducible means :Def2: :: WAYBEL_6:def 2 for x, y being Element of G holds ( not g = x "/\" y or x = g or y = g ); end; :: deftheorem Def2 defines meet-irreducible WAYBEL_6:def_2_:_ for G being non empty RelStr for g being Element of G holds ( g is meet-irreducible iff for x, y being Element of G holds ( not g = x "/\" y or x = g or y = g ) ); notation let G be non empty RelStr ; let g be Element of G; synonym irreducible g for meet-irreducible ; end; definition let G be non empty RelStr ; let g be Element of G; attrg is join-irreducible means :: WAYBEL_6:def 3 for x, y being Element of G holds ( not g = x "\/" y or x = g or y = g ); end; :: deftheorem defines join-irreducible WAYBEL_6:def_3_:_ for G being non empty RelStr for g being Element of G holds ( g is join-irreducible iff for x, y being Element of G holds ( not g = x "\/" y or x = g or y = g ) ); definition let L be non empty RelStr ; func IRR L -> Subset of L means :Def4: :: WAYBEL_6:def 4 for x being Element of L holds ( x in it iff x is irreducible ); existence ex b1 being Subset of L st for x being Element of L holds ( x in b1 iff x is irreducible ) proof defpred S1[ Element of L] means $1 is irreducible ; consider X being Subset of L such that A1: for x being Element of L holds ( x in X iff S1[x] ) from SUBSET_1:sch_3(); take X ; ::_thesis: for x being Element of L holds ( x in X iff x is irreducible ) thus for x being Element of L holds ( x in X iff x is irreducible ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of L st ( for x being Element of L holds ( x in b1 iff x is irreducible ) ) & ( for x being Element of L holds ( x in b2 iff x is irreducible ) ) holds b1 = b2 proof let X, Y be Subset of L; ::_thesis: ( ( for x being Element of L holds ( x in X iff x is irreducible ) ) & ( for x being Element of L holds ( x in Y iff x is irreducible ) ) implies X = Y ) assume that A2: for x being Element of L holds ( x in X iff x is irreducible ) and A3: for x being Element of L holds ( x in Y iff x is irreducible ) ; ::_thesis: X = Y now__::_thesis:_for_x_being_set_st_x_in_Y_holds_ x_in_X let x be set ; ::_thesis: ( x in Y implies x in X ) assume A4: x in Y ; ::_thesis: x in X then reconsider x1 = x as Element of L ; x1 is irreducible by A3, A4; hence x in X by A2; ::_thesis: verum end; then A5: Y c= X by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_X_holds_ x_in_Y let x be set ; ::_thesis: ( x in X implies x in Y ) assume A6: x in X ; ::_thesis: x in Y then reconsider x1 = x as Element of L ; x1 is irreducible by A2, A6; hence x in Y by A3; ::_thesis: verum end; then X c= Y by TARSKI:def_3; hence X = Y by A5, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def4 defines IRR WAYBEL_6:def_4_:_ for L being non empty RelStr for b2 being Subset of L holds ( b2 = IRR L iff for x being Element of L holds ( x in b2 iff x is irreducible ) ); theorem Th10: :: WAYBEL_6:10 for L being non empty antisymmetric upper-bounded with_infima RelStr holds Top L is irreducible proof let L be non empty antisymmetric upper-bounded with_infima RelStr ; ::_thesis: Top L is irreducible let x, y be Element of L; :: according to WAYBEL_6:def_2 ::_thesis: ( not Top L = x "/\" y or x = Top L or y = Top L ) assume x "/\" y = Top L ; ::_thesis: ( x = Top L or y = Top L ) then A1: ( x >= Top L & y >= Top L ) by YELLOW_0:23; ( x <= Top L or y <= Top L ) by YELLOW_0:45; hence ( x = Top L or y = Top L ) by A1, ORDERS_2:2; ::_thesis: verum end; registration let L be non empty antisymmetric upper-bounded with_infima RelStr ; cluster irreducible for Element of the carrier of L; existence ex b1 being Element of L st b1 is irreducible proof take Top L ; ::_thesis: Top L is irreducible thus Top L is irreducible by Th10; ::_thesis: verum end; end; theorem :: WAYBEL_6:11 for L being Semilattice for x being Element of L holds ( x is irreducible iff for A being non empty finite Subset of L st x = inf A holds x in A ) proof let L be Semilattice; ::_thesis: for x being Element of L holds ( x is irreducible iff for A being non empty finite Subset of L st x = inf A holds x in A ) let I be Element of L; ::_thesis: ( I is irreducible iff for A being non empty finite Subset of L st I = inf A holds I in A ) thus ( I is irreducible implies for A being non empty finite Subset of L st I = inf A holds I in A ) ::_thesis: ( ( for A being non empty finite Subset of L st I = inf A holds I in A ) implies I is irreducible ) proof defpred S1[ set ] means ( not $1 is empty & I = "/\" ($1,L) implies I in $1 ); assume A1: for x, y being Element of L holds ( not I = x "/\" y or I = x or I = y ) ; :: according to WAYBEL_6:def_2 ::_thesis: for A being non empty finite Subset of L st I = inf A holds I in A let A be non empty finite Subset of L; ::_thesis: ( I = inf A implies I in A ) A2: now__::_thesis:_for_x,_B_being_set_st_x_in_A_&_B_c=_A_&_S1[B]_holds_ S1[B_\/_{x}] let x, B be set ; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] ) assume that A3: x in A and A4: B c= A and A5: S1[B] ; ::_thesis: S1[B \/ {x}] thus S1[B \/ {x}] ::_thesis: verum proof reconsider a = x as Element of L by A3; reconsider C = B as finite Subset of L by A4, XBOOLE_1:1; assume that not B \/ {x} is empty and A6: I = "/\" ((B \/ {x}),L) ; ::_thesis: I in B \/ {x} percases ( B = {} or B <> {} ) ; supposeA7: B = {} ; ::_thesis: I in B \/ {x} then "/\" ((B \/ {a}),L) = a by YELLOW_0:39; hence I in B \/ {x} by A6, A7, TARSKI:def_1; ::_thesis: verum end; supposeA8: B <> {} ; ::_thesis: I in B \/ {x} A9: inf {a} = a by YELLOW_0:39; A10: ex_inf_of {a},L by YELLOW_0:55; ex_inf_of C,L by A8, YELLOW_0:55; then A11: "/\" ((B \/ {x}),L) = (inf C) "/\" (inf {a}) by A10, YELLOW_2:4; hereby ::_thesis: verum percases ( inf C = I or a = I ) by A1, A6, A11, A9; suppose inf C = I ; ::_thesis: I in B \/ {x} hence I in B \/ {x} by A5, A8, XBOOLE_0:def_3; ::_thesis: verum end; supposeA12: a = I ; ::_thesis: I in B \/ {x} a in {a} by TARSKI:def_1; hence I in B \/ {x} by A12, XBOOLE_0:def_3; ::_thesis: verum end; end; end; end; end; end; end; A13: S1[ {} ] ; A14: A is finite ; S1[A] from FINSET_1:sch_2(A14, A13, A2); hence ( I = inf A implies I in A ) ; ::_thesis: verum end; assume A15: for A being non empty finite Subset of L st I = inf A holds I in A ; ::_thesis: I is irreducible let a, b be Element of L; :: according to WAYBEL_6:def_2 ::_thesis: ( not I = a "/\" b or a = I or b = I ) assume I = a "/\" b ; ::_thesis: ( a = I or b = I ) then I = inf {a,b} by YELLOW_0:40; then I in {a,b} by A15; hence ( a = I or b = I ) by TARSKI:def_2; ::_thesis: verum end; theorem :: WAYBEL_6:12 for L being LATTICE for l being Element of L st (uparrow l) \ {l} is Filter of L holds l is irreducible proof let L be LATTICE; ::_thesis: for l being Element of L st (uparrow l) \ {l} is Filter of L holds l is irreducible let l be Element of L; ::_thesis: ( (uparrow l) \ {l} is Filter of L implies l is irreducible ) set F = (uparrow l) \ {l}; assume A1: (uparrow l) \ {l} is Filter of L ; ::_thesis: l is irreducible now__::_thesis:_for_x,_y_being_Element_of_L_st_l_=_x_"/\"_y_&_x_<>_l_holds_ not_y_<>_l let x, y be Element of L; ::_thesis: ( l = x "/\" y & x <> l implies not y <> l ) assume that A2: l = x "/\" y and A3: x <> l and A4: y <> l ; ::_thesis: contradiction l <= y by A2, YELLOW_0:23; then y in uparrow l by WAYBEL_0:18; then A5: y in (uparrow l) \ {l} by A4, ZFMISC_1:56; l <= x by A2, YELLOW_0:23; then x in uparrow l by WAYBEL_0:18; then x in (uparrow l) \ {l} by A3, ZFMISC_1:56; then consider z being Element of L such that A6: z in (uparrow l) \ {l} and A7: ( z <= x & z <= y ) by A1, A5, WAYBEL_0:def_2; l >= z by A2, A7, YELLOW_0:23; then l in (uparrow l) \ {l} by A1, A6, WAYBEL_0:def_20; hence contradiction by ZFMISC_1:56; ::_thesis: verum end; hence l is irreducible by Def2; ::_thesis: verum end; theorem Th13: :: WAYBEL_6:13 for L being LATTICE for p being Element of L for F being Filter of L st p is_maximal_in F ` holds p is irreducible proof let L be LATTICE; ::_thesis: for p being Element of L for F being Filter of L st p is_maximal_in F ` holds p is irreducible let p be Element of L; ::_thesis: for F being Filter of L st p is_maximal_in F ` holds p is irreducible let F be Filter of L; ::_thesis: ( p is_maximal_in F ` implies p is irreducible ) assume A1: p is_maximal_in F ` ; ::_thesis: p is irreducible set X = the carrier of L \ F; A2: p in the carrier of L \ F by A1, WAYBEL_4:55; now__::_thesis:_for_x,_y_being_Element_of_L_st_p_=_x_"/\"_y_&_x_<>_p_holds_ not_y_<>_p let x, y be Element of L; ::_thesis: ( p = x "/\" y & x <> p implies not y <> p ) assume that A3: p = x "/\" y and A4: x <> p and A5: y <> p ; ::_thesis: contradiction p <= y by A3, YELLOW_0:23; then A6: p < y by A5, ORDERS_2:def_6; now__::_thesis:_(_x_in_F_implies_not_y_in_F_) assume ( x in F & y in F ) ; ::_thesis: contradiction then consider z being Element of L such that A7: z in F and A8: ( z <= x & z <= y ) by WAYBEL_0:def_2; p >= z by A3, A8, YELLOW_0:23; then p in F by A7, WAYBEL_0:def_20; hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum end; then A9: ( x in the carrier of L \ F or y in the carrier of L \ F ) by XBOOLE_0:def_5; p <= x by A3, YELLOW_0:23; then p < x by A4, ORDERS_2:def_6; hence contradiction by A1, A9, A6, WAYBEL_4:55; ::_thesis: verum end; hence p is irreducible by Def2; ::_thesis: verum end; theorem Th14: :: WAYBEL_6:14 for L being lower-bounded continuous LATTICE for x, y being Element of L st not y <= x holds ex p being Element of L st ( p is irreducible & x <= p & not y <= p ) proof let L be lower-bounded continuous LATTICE; ::_thesis: for x, y being Element of L st not y <= x holds ex p being Element of L st ( p is irreducible & x <= p & not y <= p ) let x, y be Element of L; ::_thesis: ( not y <= x implies ex p being Element of L st ( p is irreducible & x <= p & not y <= p ) ) assume A1: not y <= x ; ::_thesis: ex p being Element of L st ( p is irreducible & x <= p & not y <= p ) for x being Element of L holds ( not waybelow x is empty & waybelow x is directed ) ; then consider u being Element of L such that A2: u << y and A3: not u <= x by A1, WAYBEL_3:24; consider F being Open Filter of L such that A4: y in F and A5: F c= wayabove u by A2, Th8; A6: wayabove u c= uparrow u by WAYBEL_3:11; now__::_thesis:_not_x_in_F assume x in F ; ::_thesis: contradiction then x in uparrow u by A5, A6, TARSKI:def_3; hence contradiction by A3, WAYBEL_0:18; ::_thesis: verum end; then x in the carrier of L \ F by XBOOLE_0:def_5; then consider m being Element of L such that A7: x <= m and A8: m is_maximal_in F ` by Th9; take m ; ::_thesis: ( m is irreducible & x <= m & not y <= m ) A9: m in F ` by A8, WAYBEL_4:55; now__::_thesis:_not_y_<=_m assume y <= m ; ::_thesis: contradiction then m in F by A4, WAYBEL_0:def_20; hence contradiction by A9, XBOOLE_0:def_5; ::_thesis: verum end; hence ( m is irreducible & x <= m & not y <= m ) by A7, A8, Th13; ::_thesis: verum end; begin definition let L be non empty RelStr ; let X be Subset of L; attrX is order-generating means :Def5: :: WAYBEL_6:def 5 for x being Element of L holds ( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) ); end; :: deftheorem Def5 defines order-generating WAYBEL_6:def_5_:_ for L being non empty RelStr for X being Subset of L holds ( X is order-generating iff for x being Element of L holds ( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) ) ); theorem Th15: :: WAYBEL_6:15 for L being lower-bounded up-complete LATTICE for X being Subset of L holds ( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) proof let L be lower-bounded up-complete LATTICE; ::_thesis: for X being Subset of L holds ( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) let X be Subset of L; ::_thesis: ( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) thus ( X is order-generating implies for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) ::_thesis: ( ( for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) implies X is order-generating ) proof assume A1: X is order-generating ; ::_thesis: for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) let l be Element of L; ::_thesis: ex Y being Subset of X st l = "/\" (Y,L) for x being set st x in (uparrow l) /\ X holds x in X by XBOOLE_0:def_4; then reconsider Y = (uparrow l) /\ X as Subset of X by TARSKI:def_3; l = "/\" (Y,L) by A1, Def5; hence ex Y being Subset of X st l = "/\" (Y,L) ; ::_thesis: verum end; thus ( ( for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) implies X is order-generating ) ::_thesis: verum proof assume A2: for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ; ::_thesis: X is order-generating let l be Element of L; :: according to WAYBEL_6:def_5 ::_thesis: ( ex_inf_of (uparrow l) /\ X,L & l = inf ((uparrow l) /\ X) ) consider Y being Subset of X such that A3: l = "/\" (Y,L) by A2; set S = (uparrow l) /\ X; thus ex_inf_of (uparrow l) /\ X,L by YELLOW_0:17; ::_thesis: l = inf ((uparrow l) /\ X) A4: for b being Element of L st b is_<=_than (uparrow l) /\ X holds b <= l proof let b be Element of L; ::_thesis: ( b is_<=_than (uparrow l) /\ X implies b <= l ) assume A5: b is_<=_than (uparrow l) /\ X ; ::_thesis: b <= l now__::_thesis:_for_x_being_Element_of_L_st_x_in_Y_holds_ b_<=_x let x be Element of L; ::_thesis: ( x in Y implies b <= x ) assume A6: x in Y ; ::_thesis: b <= x l is_<=_than Y by A3, YELLOW_0:33; then l <= x by A6, LATTICE3:def_8; then x in uparrow l by WAYBEL_0:18; then x in (uparrow l) /\ X by A6, XBOOLE_0:def_4; hence b <= x by A5, LATTICE3:def_8; ::_thesis: verum end; then b is_<=_than Y by LATTICE3:def_8; hence b <= l by A3, YELLOW_0:33; ::_thesis: verum end; now__::_thesis:_for_x_being_Element_of_L_st_x_in_(uparrow_l)_/\_X_holds_ l_<=_x let x be Element of L; ::_thesis: ( x in (uparrow l) /\ X implies l <= x ) assume x in (uparrow l) /\ X ; ::_thesis: l <= x then x in uparrow l by XBOOLE_0:def_4; hence l <= x by WAYBEL_0:18; ::_thesis: verum end; then l is_<=_than (uparrow l) /\ X by LATTICE3:def_8; hence l = inf ((uparrow l) /\ X) by A4, YELLOW_0:33; ::_thesis: verum end; end; theorem :: WAYBEL_6:16 for L being lower-bounded up-complete LATTICE for X being Subset of L holds ( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds the carrier of L = Y ) proof let L be lower-bounded up-complete LATTICE; ::_thesis: for X being Subset of L holds ( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds the carrier of L = Y ) let X be Subset of L; ::_thesis: ( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds the carrier of L = Y ) thus ( X is order-generating implies for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds the carrier of L = Y ) ::_thesis: ( ( for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds the carrier of L = Y ) implies X is order-generating ) proof assume A1: X is order-generating ; ::_thesis: for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds the carrier of L = Y let Y be Subset of L; ::_thesis: ( X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) implies the carrier of L = Y ) assume that A2: X c= Y and A3: for Z being Subset of Y holds "/\" (Z,L) in Y ; ::_thesis: the carrier of L = Y now__::_thesis:_for_l1_being_set_st_l1_in_the_carrier_of_L_holds_ l1_in_Y let l1 be set ; ::_thesis: ( l1 in the carrier of L implies l1 in Y ) assume l1 in the carrier of L ; ::_thesis: l1 in Y then reconsider l = l1 as Element of L ; ( (uparrow l) /\ Y c= Y & (uparrow l) /\ X c= (uparrow l) /\ Y ) by A2, XBOOLE_1:17, XBOOLE_1:26; then A4: (uparrow l) /\ X c= Y by XBOOLE_1:1; l = inf ((uparrow l) /\ X) by A1, Def5; hence l1 in Y by A3, A4; ::_thesis: verum end; hence the carrier of L c= Y by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: Y c= the carrier of L thus Y c= the carrier of L ; ::_thesis: verum end; thus ( ( for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds the carrier of L = Y ) implies X is order-generating ) ::_thesis: verum proof set Y = { ("/\" (Z,L)) where Z is Subset of L : Z c= X } ; now__::_thesis:_for_x_being_set_st_x_in__{__("/\"_(Z,L))_where_Z_is_Subset_of_L_:_Z_c=_X__}__holds_ x_in_the_carrier_of_L let x be set ; ::_thesis: ( x in { ("/\" (Z,L)) where Z is Subset of L : Z c= X } implies x in the carrier of L ) assume x in { ("/\" (Z,L)) where Z is Subset of L : Z c= X } ; ::_thesis: x in the carrier of L then ex Z being Subset of L st ( x = "/\" (Z,L) & Z c= X ) ; hence x in the carrier of L ; ::_thesis: verum end; then reconsider Y = { ("/\" (Z,L)) where Z is Subset of L : Z c= X } as Subset of L by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_X_holds_ x_in_Y let x be set ; ::_thesis: ( x in X implies x in Y ) assume A5: x in X ; ::_thesis: x in Y then reconsider x1 = x as Element of L ; reconsider x2 = {x1} as Subset of L ; A6: x1 = "/\" (x2,L) by YELLOW_0:39; {x1} c= X by A5, ZFMISC_1:31; hence x in Y by A6; ::_thesis: verum end; then A7: X c= Y by TARSKI:def_3; assume A8: for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds the carrier of L = Y ; ::_thesis: X is order-generating for l being Element of L ex Z being Subset of X st l = "/\" (Z,L) proof let l be Element of L; ::_thesis: ex Z being Subset of X st l = "/\" (Z,L) for Z being Subset of Y holds "/\" (Z,L) in Y proof let Z be Subset of Y; ::_thesis: "/\" (Z,L) in Y set S = union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ; now__::_thesis:_for_x_being_set_st_x_in_union__{__A_where_A_is_Subset_of_L_:_(_A_c=_X_&_"/\"_(A,L)_in_Z_)__}__holds_ x_in_the_carrier_of_L let x be set ; ::_thesis: ( x in union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } implies x in the carrier of L ) assume x in union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ; ::_thesis: x in the carrier of L then consider Y being set such that A9: x in Y and A10: Y in { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } by TARSKI:def_4; ex A being Subset of L st ( Y = A & A c= X & "/\" (A,L) in Z ) by A10; hence x in the carrier of L by A9; ::_thesis: verum end; then reconsider S = union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } as Subset of L by TARSKI:def_3; defpred S1[ Subset of L] means ( $1 c= X & "/\" ($1,L) in Z ); set N = { ("/\" (A,L)) where A is Subset of L : S1[A] } ; now__::_thesis:_for_x_being_set_st_x_in_Z_holds_ x_in__{__("/\"_(A,L))_where_A_is_Subset_of_L_:_S1[A]__}_ let x be set ; ::_thesis: ( x in Z implies x in { ("/\" (A,L)) where A is Subset of L : S1[A] } ) assume A11: x in Z ; ::_thesis: x in { ("/\" (A,L)) where A is Subset of L : S1[A] } then x in Y ; then ex Z being Subset of L st ( x = "/\" (Z,L) & Z c= X ) ; hence x in { ("/\" (A,L)) where A is Subset of L : S1[A] } by A11; ::_thesis: verum end; then A12: Z c= { ("/\" (A,L)) where A is Subset of L : S1[A] } by TARSKI:def_3; now__::_thesis:_for_B_being_set_st_B_in__{__A_where_A_is_Subset_of_L_:_(_A_c=_X_&_"/\"_(A,L)_in_Z_)__}__holds_ B_c=_X let B be set ; ::_thesis: ( B in { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } implies B c= X ) assume B in { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ; ::_thesis: B c= X then ex A being Subset of L st ( B = A & A c= X & "/\" (A,L) in Z ) ; hence B c= X ; ::_thesis: verum end; then A13: S c= X by ZFMISC_1:76; now__::_thesis:_for_x_being_set_st_x_in__{__("/\"_(A,L))_where_A_is_Subset_of_L_:_S1[A]__}__holds_ x_in_Z let x be set ; ::_thesis: ( x in { ("/\" (A,L)) where A is Subset of L : S1[A] } implies x in Z ) assume x in { ("/\" (A,L)) where A is Subset of L : S1[A] } ; ::_thesis: x in Z then ex S being Subset of L st ( x = "/\" (S,L) & S c= X & "/\" (S,L) in Z ) ; hence x in Z ; ::_thesis: verum end; then { ("/\" (A,L)) where A is Subset of L : S1[A] } c= Z by TARSKI:def_3; then "/\" (Z,L) = "/\" ( { ("/\" (A,L)) where A is Subset of L : S1[A] } ,L) by A12, XBOOLE_0:def_10 .= "/\" ((union { A where A is Subset of L : S1[A] } ),L) from YELLOW_3:sch_3() ; hence "/\" (Z,L) in Y by A13; ::_thesis: verum end; then the carrier of L = Y by A8, A7; then l in Y ; then ex Z being Subset of L st ( l = "/\" (Z,L) & Z c= X ) ; hence ex Z being Subset of X st l = "/\" (Z,L) ; ::_thesis: verum end; hence X is order-generating by Th15; ::_thesis: verum end; end; theorem Th17: :: WAYBEL_6:17 for L being lower-bounded up-complete LATTICE for X being Subset of L holds ( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) ) proof let L be lower-bounded up-complete LATTICE; ::_thesis: for X being Subset of L holds ( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) ) let X be Subset of L; ::_thesis: ( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) ) thus ( X is order-generating implies for l1, l2 being Element of L st not l2 <= l1 holds ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) ) ::_thesis: ( ( for l1, l2 being Element of L st not l2 <= l1 holds ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) ) implies X is order-generating ) proof assume A1: X is order-generating ; ::_thesis: for l1, l2 being Element of L st not l2 <= l1 holds ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) let l1, l2 be Element of L; ::_thesis: ( not l2 <= l1 implies ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) ) consider P being Subset of X such that A2: l1 = "/\" (P,L) by A1, Th15; assume A3: not l2 <= l1 ; ::_thesis: ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) now__::_thesis:_ex_p_being_Element_of_L_st_ (_p_in_P_&_not_l2_<=_p_) assume for p being Element of L st p in P holds l2 <= p ; ::_thesis: contradiction then l2 is_<=_than P by LATTICE3:def_8; hence contradiction by A3, A2, YELLOW_0:33; ::_thesis: verum end; then consider p being Element of L such that A4: ( p in P & not l2 <= p ) ; take p ; ::_thesis: ( p in X & l1 <= p & not l2 <= p ) l1 is_<=_than P by A2, YELLOW_0:33; hence ( p in X & l1 <= p & not l2 <= p ) by A4, LATTICE3:def_8; ::_thesis: verum end; thus ( ( for l1, l2 being Element of L st not l2 <= l1 holds ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) ) implies X is order-generating ) ::_thesis: verum proof assume A5: for l1, l2 being Element of L st not l2 <= l1 holds ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) ; ::_thesis: X is order-generating let l be Element of L; :: according to WAYBEL_6:def_5 ::_thesis: ( ex_inf_of (uparrow l) /\ X,L & l = inf ((uparrow l) /\ X) ) set y = inf ((uparrow l) /\ X); thus ex_inf_of (uparrow l) /\ X,L by YELLOW_0:17; ::_thesis: l = inf ((uparrow l) /\ X) A6: inf ((uparrow l) /\ X) is_<=_than (uparrow l) /\ X by YELLOW_0:33; now__::_thesis:_not_inf_((uparrow_l)_/\_X)_<>_l l is_<=_than (uparrow l) /\ X proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in (uparrow l) /\ X or l <= b ) assume b in (uparrow l) /\ X ; ::_thesis: l <= b then b in uparrow l by XBOOLE_0:def_4; hence l <= b by WAYBEL_0:18; ::_thesis: verum end; then l <= inf ((uparrow l) /\ X) by YELLOW_0:33; then A7: not inf ((uparrow l) /\ X) < l by ORDERS_2:6; assume A8: inf ((uparrow l) /\ X) <> l ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( not inf ((uparrow l) /\ X) <= l or inf ((uparrow l) /\ X) = l ) by A7, ORDERS_2:def_6; suppose not inf ((uparrow l) /\ X) <= l ; ::_thesis: contradiction then consider p being Element of L such that A9: p in X and A10: l <= p and A11: not inf ((uparrow l) /\ X) <= p by A5; p in uparrow l by A10, WAYBEL_0:18; then p in (uparrow l) /\ X by A9, XBOOLE_0:def_4; hence contradiction by A6, A11, LATTICE3:def_8; ::_thesis: verum end; suppose inf ((uparrow l) /\ X) = l ; ::_thesis: contradiction hence contradiction by A8; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence l = inf ((uparrow l) /\ X) ; ::_thesis: verum end; end; theorem Th18: :: WAYBEL_6:18 for L being lower-bounded continuous LATTICE for X being Subset of L st X = (IRR L) \ {(Top L)} holds X is order-generating proof let L be lower-bounded continuous LATTICE; ::_thesis: for X being Subset of L st X = (IRR L) \ {(Top L)} holds X is order-generating let X be Subset of L; ::_thesis: ( X = (IRR L) \ {(Top L)} implies X is order-generating ) assume A1: X = (IRR L) \ {(Top L)} ; ::_thesis: X is order-generating for l1, l2 being Element of L st not l2 <= l1 holds ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) proof let x, y be Element of L; ::_thesis: ( not y <= x implies ex p being Element of L st ( p in X & x <= p & not y <= p ) ) assume not y <= x ; ::_thesis: ex p being Element of L st ( p in X & x <= p & not y <= p ) then consider p being Element of L such that A2: p is irreducible and A3: x <= p and A4: not y <= p by Th14; ( p <> Top L & p in IRR L ) by A2, A4, Def4, YELLOW_0:45; then p in X by A1, ZFMISC_1:56; hence ex p being Element of L st ( p in X & x <= p & not y <= p ) by A3, A4; ::_thesis: verum end; hence X is order-generating by Th17; ::_thesis: verum end; theorem Th19: :: WAYBEL_6:19 for L being lower-bounded continuous LATTICE for X, Y being Subset of L st X is order-generating & X c= Y holds Y is order-generating proof let L be lower-bounded continuous LATTICE; ::_thesis: for X, Y being Subset of L st X is order-generating & X c= Y holds Y is order-generating let X, Y be Subset of L; ::_thesis: ( X is order-generating & X c= Y implies Y is order-generating ) assume that A1: X is order-generating and A2: X c= Y ; ::_thesis: Y is order-generating let x be Element of L; :: according to WAYBEL_6:def_5 ::_thesis: ( ex_inf_of (uparrow x) /\ Y,L & x = inf ((uparrow x) /\ Y) ) thus ex_inf_of (uparrow x) /\ Y,L by YELLOW_0:17; ::_thesis: x = inf ((uparrow x) /\ Y) A3: ex_inf_of (uparrow x) /\ Y,L by YELLOW_0:17; ex_inf_of uparrow x,L by WAYBEL_0:39; then inf ((uparrow x) /\ Y) >= inf (uparrow x) by A3, XBOOLE_1:17, YELLOW_0:35; then A4: inf ((uparrow x) /\ Y) >= x by WAYBEL_0:39; ex_inf_of (uparrow x) /\ X,L by YELLOW_0:17; then inf ((uparrow x) /\ X) >= inf ((uparrow x) /\ Y) by A2, A3, XBOOLE_1:26, YELLOW_0:35; then x >= inf ((uparrow x) /\ Y) by A1, Def5; hence x = inf ((uparrow x) /\ Y) by A4, ORDERS_2:2; ::_thesis: verum end; begin definition let L be non empty RelStr ; let l be Element of L; attrl is prime means :Def6: :: WAYBEL_6:def 6 for x, y being Element of L holds ( not x "/\" y <= l or x <= l or y <= l ); end; :: deftheorem Def6 defines prime WAYBEL_6:def_6_:_ for L being non empty RelStr for l being Element of L holds ( l is prime iff for x, y being Element of L holds ( not x "/\" y <= l or x <= l or y <= l ) ); definition let L be non empty RelStr ; func PRIME L -> Subset of L means :Def7: :: WAYBEL_6:def 7 for x being Element of L holds ( x in it iff x is prime ); existence ex b1 being Subset of L st for x being Element of L holds ( x in b1 iff x is prime ) proof defpred S1[ Element of L] means $1 is prime ; consider X being Subset of L such that A1: for x being Element of L holds ( x in X iff S1[x] ) from SUBSET_1:sch_3(); take X ; ::_thesis: for x being Element of L holds ( x in X iff x is prime ) thus for x being Element of L holds ( x in X iff x is prime ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of L st ( for x being Element of L holds ( x in b1 iff x is prime ) ) & ( for x being Element of L holds ( x in b2 iff x is prime ) ) holds b1 = b2 proof let X, Y be Subset of L; ::_thesis: ( ( for x being Element of L holds ( x in X iff x is prime ) ) & ( for x being Element of L holds ( x in Y iff x is prime ) ) implies X = Y ) assume that A2: for x being Element of L holds ( x in X iff x is prime ) and A3: for x being Element of L holds ( x in Y iff x is prime ) ; ::_thesis: X = Y thus X c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y ) assume A4: x in X ; ::_thesis: x in Y then reconsider x1 = x as Element of L ; x1 is prime by A2, A4; hence x in Y by A3; ::_thesis: verum end; thus Y c= X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in X ) assume A5: x in Y ; ::_thesis: x in X then reconsider x1 = x as Element of L ; x1 is prime by A3, A5; hence x in X by A2; ::_thesis: verum end; end; end; :: deftheorem Def7 defines PRIME WAYBEL_6:def_7_:_ for L being non empty RelStr for b2 being Subset of L holds ( b2 = PRIME L iff for x being Element of L holds ( x in b2 iff x is prime ) ); definition let L be non empty RelStr ; let l be Element of L; attrl is co-prime means :Def8: :: WAYBEL_6:def 8 l ~ is prime ; end; :: deftheorem Def8 defines co-prime WAYBEL_6:def_8_:_ for L being non empty RelStr for l being Element of L holds ( l is co-prime iff l ~ is prime ); theorem Th20: :: WAYBEL_6:20 for L being non empty antisymmetric upper-bounded RelStr holds Top L is prime proof let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: Top L is prime let x, y be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not x "/\" y <= Top L or x <= Top L or y <= Top L ) assume x "/\" y <= Top L ; ::_thesis: ( x <= Top L or y <= Top L ) thus ( x <= Top L or y <= Top L ) by YELLOW_0:45; ::_thesis: verum end; theorem :: WAYBEL_6:21 for L being non empty antisymmetric lower-bounded RelStr holds Bottom L is co-prime proof let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: Bottom L is co-prime Top (L ~) is prime by Th20; hence (Bottom L) ~ is prime by YELLOW_7:33; :: according to WAYBEL_6:def_8 ::_thesis: verum end; registration let L be non empty antisymmetric upper-bounded RelStr ; cluster prime for Element of the carrier of L; existence ex b1 being Element of L st b1 is prime proof take Top L ; ::_thesis: Top L is prime thus Top L is prime by Th20; ::_thesis: verum end; end; theorem Th22: :: WAYBEL_6:22 for L being Semilattice for l being Element of L holds ( l is prime iff for A being non empty finite Subset of L st l >= inf A holds ex a being Element of L st ( a in A & l >= a ) ) proof let L be Semilattice; ::_thesis: for l being Element of L holds ( l is prime iff for A being non empty finite Subset of L st l >= inf A holds ex a being Element of L st ( a in A & l >= a ) ) let l be Element of L; ::_thesis: ( l is prime iff for A being non empty finite Subset of L st l >= inf A holds ex a being Element of L st ( a in A & l >= a ) ) thus ( l is prime implies for A being non empty finite Subset of L st l >= inf A holds ex a being Element of L st ( a in A & l >= a ) ) ::_thesis: ( ( for A being non empty finite Subset of L st l >= inf A holds ex a being Element of L st ( a in A & l >= a ) ) implies l is prime ) proof defpred S1[ set ] means ( not $1 is empty & l >= "/\" ($1,L) implies ex k being Element of L st ( k in $1 & l >= k ) ); assume A1: for x, y being Element of L holds ( not l >= x "/\" y or l >= x or l >= y ) ; :: according to WAYBEL_6:def_6 ::_thesis: for A being non empty finite Subset of L st l >= inf A holds ex a being Element of L st ( a in A & l >= a ) let A be non empty finite Subset of L; ::_thesis: ( l >= inf A implies ex a being Element of L st ( a in A & l >= a ) ) A2: now__::_thesis:_for_x,_B_being_set_st_x_in_A_&_B_c=_A_&_S1[B]_holds_ S1[B_\/_{x}] let x, B be set ; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] ) assume that A3: x in A and A4: B c= A and A5: S1[B] ; ::_thesis: S1[B \/ {x}] thus S1[B \/ {x}] ::_thesis: verum proof reconsider a = x as Element of L by A3; reconsider C = B as finite Subset of L by A4, XBOOLE_1:1; assume that not B \/ {x} is empty and A6: l >= "/\" ((B \/ {x}),L) ; ::_thesis: ex k being Element of L st ( k in B \/ {x} & l >= k ) percases ( B = {} or B <> {} ) ; suppose B = {} ; ::_thesis: ex k being Element of L st ( k in B \/ {x} & l >= k ) then ( "/\" ((B \/ {a}),L) = a & a in B \/ {a} ) by TARSKI:def_1, YELLOW_0:39; hence ex k being Element of L st ( k in B \/ {x} & l >= k ) by A6; ::_thesis: verum end; supposeA7: B <> {} ; ::_thesis: ex k being Element of L st ( k in B \/ {x} & l >= k ) A8: inf {a} = a by YELLOW_0:39; A9: ex_inf_of {a},L by YELLOW_0:55; ex_inf_of C,L by A7, YELLOW_0:55; then A10: "/\" ((B \/ {x}),L) = (inf C) "/\" (inf {a}) by A9, YELLOW_2:4; hereby ::_thesis: verum percases ( inf C <= l or a <= l ) by A1, A6, A10, A8; suppose inf C <= l ; ::_thesis: ex k being Element of L st ( k in B \/ {x} & l >= k ) then consider b being Element of L such that A11: b in B and A12: b <= l by A5, A7; b in B \/ {x} by A11, XBOOLE_0:def_3; hence ex k being Element of L st ( k in B \/ {x} & l >= k ) by A12; ::_thesis: verum end; supposeA13: a <= l ; ::_thesis: ex k being Element of L st ( k in B \/ {x} & l >= k ) a in {a} by TARSKI:def_1; then a in B \/ {x} by XBOOLE_0:def_3; hence ex k being Element of L st ( k in B \/ {x} & l >= k ) by A13; ::_thesis: verum end; end; end; end; end; end; end; A14: S1[ {} ] ; A15: A is finite ; S1[A] from FINSET_1:sch_2(A15, A14, A2); hence ( l >= inf A implies ex a being Element of L st ( a in A & l >= a ) ) ; ::_thesis: verum end; assume A16: for A being non empty finite Subset of L st l >= inf A holds ex a being Element of L st ( a in A & l >= a ) ; ::_thesis: l is prime let a, b be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not a "/\" b <= l or a <= l or b <= l ) set A = {a,b}; A17: inf {a,b} = a "/\" b by YELLOW_0:40; assume a "/\" b <= l ; ::_thesis: ( a <= l or b <= l ) then ex k being Element of L st ( k in {a,b} & l >= k ) by A16, A17; hence ( a <= l or b <= l ) by TARSKI:def_2; ::_thesis: verum end; theorem Th23: :: WAYBEL_6:23 for L being sup-Semilattice for x being Element of L holds ( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds ex a being Element of L st ( a in A & x <= a ) ) proof let L be sup-Semilattice; ::_thesis: for x being Element of L holds ( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds ex a being Element of L st ( a in A & x <= a ) ) let x be Element of L; ::_thesis: ( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds ex a being Element of L st ( a in A & x <= a ) ) thus ( x is co-prime implies for A being non empty finite Subset of L st x <= sup A holds ex a being Element of L st ( a in A & x <= a ) ) ::_thesis: ( ( for A being non empty finite Subset of L st x <= sup A holds ex a being Element of L st ( a in A & x <= a ) ) implies x is co-prime ) proof assume x is co-prime ; ::_thesis: for A being non empty finite Subset of L st x <= sup A holds ex a being Element of L st ( a in A & x <= a ) then A1: x ~ is prime by Def8; let A be non empty finite Subset of L; ::_thesis: ( x <= sup A implies ex a being Element of L st ( a in A & x <= a ) ) reconsider A1 = A as non empty finite Subset of (L ~) ; assume x <= sup A ; ::_thesis: ex a being Element of L st ( a in A & x <= a ) then A2: x ~ >= (sup A) ~ by LATTICE3:9; A3: ex_sup_of A,L by YELLOW_0:54; then "\/" (A,L) is_>=_than A by YELLOW_0:def_9; then A4: ("\/" (A,L)) ~ is_<=_than A by YELLOW_7:8; A5: now__::_thesis:_for_y_being_Element_of_(L_~)_st_y_is_<=_than_A_holds_ y_<=_("\/"_(A,L))_~ let y be Element of (L ~); ::_thesis: ( y is_<=_than A implies y <= ("\/" (A,L)) ~ ) assume y is_<=_than A ; ::_thesis: y <= ("\/" (A,L)) ~ then ~ y is_>=_than A by YELLOW_7:9; then ~ y >= "\/" (A,L) by A3, YELLOW_0:def_9; hence y <= ("\/" (A,L)) ~ by YELLOW_7:2; ::_thesis: verum end; ex_inf_of A,L ~ by A3, YELLOW_7:10; then (sup A) ~ = inf A1 by A4, A5, YELLOW_0:def_10; then consider a being Element of (L ~) such that A6: ( a in A1 & x ~ >= a ) by A1, A2, Th22; take ~ a ; ::_thesis: ( ~ a in A & x <= ~ a ) thus ( ~ a in A & x <= ~ a ) by A6, YELLOW_7:2; ::_thesis: verum end; thus ( ( for A being non empty finite Subset of L st x <= sup A holds ex a being Element of L st ( a in A & x <= a ) ) implies x is co-prime ) ::_thesis: verum proof assume A7: for A being non empty finite Subset of L st x <= sup A holds ex a being Element of L st ( a in A & x <= a ) ; ::_thesis: x is co-prime now__::_thesis:_for_a,_b_being_Element_of_(L_~)_holds_ (_not_a_"/\"_b_<=_x_~_or_a_<=_x_~_or_b_<=_x_~_) let a, b be Element of (L ~); ::_thesis: ( not a "/\" b <= x ~ or a <= x ~ or b <= x ~ ) set A = {(~ a),(~ b)}; assume a "/\" b <= x ~ ; ::_thesis: ( a <= x ~ or b <= x ~ ) then x <= ~ (a "/\" b) by YELLOW_7:2; then ( sup {(~ a),(~ b)} = (~ a) "\/" (~ b) & x <= (~ a) "\/" (~ b) ) by YELLOW_0:41, YELLOW_7:24; then consider l being Element of L such that A8: l in {(~ a),(~ b)} and A9: x <= l by A7; ( l = ~ a or l = ~ b ) by A8, TARSKI:def_2; hence ( a <= x ~ or b <= x ~ ) by A9, YELLOW_7:2; ::_thesis: verum end; then x ~ is prime by Def6; hence x is co-prime by Def8; ::_thesis: verum end; end; theorem Th24: :: WAYBEL_6:24 for L being LATTICE for l being Element of L st l is prime holds l is irreducible proof let L be LATTICE; ::_thesis: for l being Element of L st l is prime holds l is irreducible let l be Element of L; ::_thesis: ( l is prime implies l is irreducible ) assume A1: l is prime ; ::_thesis: l is irreducible let x, y be Element of L; :: according to WAYBEL_6:def_2 ::_thesis: ( not l = x "/\" y or x = l or y = l ) assume A2: l = x "/\" y ; ::_thesis: ( x = l or y = l ) then x "/\" y <= l ; then A3: ( x <= l or y <= l ) by A1, Def6; ( l <= x & l <= y ) by A2, YELLOW_0:23; hence ( x = l or y = l ) by A3, ORDERS_2:2; ::_thesis: verum end; theorem Th25: :: WAYBEL_6:25 for L being LATTICE for l being Element of L holds ( l is prime iff for x being set for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds ( f . p = {} iff p <= l ) ) holds ( f is meet-preserving & f is join-preserving ) ) proof let L be LATTICE; ::_thesis: for l being Element of L holds ( l is prime iff for x being set for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds ( f . p = {} iff p <= l ) ) holds ( f is meet-preserving & f is join-preserving ) ) let l be Element of L; ::_thesis: ( l is prime iff for x being set for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds ( f . p = {} iff p <= l ) ) holds ( f is meet-preserving & f is join-preserving ) ) thus ( l is prime implies for x being set for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds ( f . p = {} iff p <= l ) ) holds ( f is meet-preserving & f is join-preserving ) ) ::_thesis: ( ( for x being set for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds ( f . p = {} iff p <= l ) ) holds ( f is meet-preserving & f is join-preserving ) ) implies l is prime ) proof assume A1: l is prime ; ::_thesis: for x being set for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds ( f . p = {} iff p <= l ) ) holds ( f is meet-preserving & f is join-preserving ) let x be set ; ::_thesis: for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds ( f . p = {} iff p <= l ) ) holds ( f is meet-preserving & f is join-preserving ) let f be Function of L,(BoolePoset {x}); ::_thesis: ( ( for p being Element of L holds ( f . p = {} iff p <= l ) ) implies ( f is meet-preserving & f is join-preserving ) ) assume A2: for p being Element of L holds ( f . p = {} iff p <= l ) ; ::_thesis: ( f is meet-preserving & f is join-preserving ) A3: the carrier of (BoolePoset {x}) = the carrier of (InclPoset (bool {x})) by YELLOW_1:4 .= bool {x} by YELLOW_1:1 .= {{},{x}} by ZFMISC_1:24 ; A4: dom f = the carrier of L by FUNCT_2:def_1; for z, y being Element of L holds f preserves_inf_of {z,y} proof let z, y be Element of L; ::_thesis: f preserves_inf_of {z,y} A5: f .: {z,y} = {(f . z),(f . y)} by A4, FUNCT_1:60; then A6: ( ex_inf_of {z,y},L implies ex_inf_of f .: {z,y}, BoolePoset {x} ) by YELLOW_0:21; A7: now__::_thesis:_(f_._z)_"/\"_(f_._y)_=_f_._(z_"/\"_y) percases ( ( f . z = {} & f . y = {} ) or ( f . z = {x} & f . y = {x} ) or ( f . z = {} & f . y = {x} ) or ( f . z = {x} & f . y = {} ) ) by A3, TARSKI:def_2; supposeA8: ( f . z = {} & f . y = {} ) ; ::_thesis: (f . z) "/\" (f . y) = f . (z "/\" y) then ( z "/\" y <= z & z <= l ) by A2, YELLOW_0:23; then A9: z "/\" y <= l by ORDERS_2:3; thus (f . z) "/\" (f . y) = {} /\ {} by A8, YELLOW_1:17 .= f . (z "/\" y) by A2, A9 ; ::_thesis: verum end; supposeA10: ( f . z = {x} & f . y = {x} ) ; ::_thesis: (f . z) "/\" (f . y) = f . (z "/\" y) then ( not y <= l & not z <= l ) by A2; then not z "/\" y <= l by A1, Def6; then A11: not f . (z "/\" y) = {} by A2; thus (f . z) "/\" (f . y) = {x} /\ {x} by A10, YELLOW_1:17 .= f . (z "/\" y) by A3, A11, TARSKI:def_2 ; ::_thesis: verum end; supposeA12: ( f . z = {} & f . y = {x} ) ; ::_thesis: (f . z) "/\" (f . y) = f . (z "/\" y) then ( z "/\" y <= z & z <= l ) by A2, YELLOW_0:23; then A13: z "/\" y <= l by ORDERS_2:3; thus (f . z) "/\" (f . y) = {} /\ {x} by A12, YELLOW_1:17 .= f . (z "/\" y) by A2, A13 ; ::_thesis: verum end; supposeA14: ( f . z = {x} & f . y = {} ) ; ::_thesis: (f . z) "/\" (f . y) = f . (z "/\" y) then ( z "/\" y <= y & y <= l ) by A2, YELLOW_0:23; then A15: z "/\" y <= l by ORDERS_2:3; thus (f . z) "/\" (f . y) = {x} /\ {} by A14, YELLOW_1:17 .= f . (z "/\" y) by A2, A15 ; ::_thesis: verum end; end; end; inf (f .: {z,y}) = (f . z) "/\" (f . y) by A5, YELLOW_0:40 .= f . (inf {z,y}) by A7, YELLOW_0:40 ; hence f preserves_inf_of {z,y} by A6, WAYBEL_0:def_30; ::_thesis: verum end; hence f is meet-preserving by WAYBEL_0:def_34; ::_thesis: f is join-preserving for z, y being Element of L holds f preserves_sup_of {z,y} proof let z, y be Element of L; ::_thesis: f preserves_sup_of {z,y} A16: f .: {z,y} = {(f . z),(f . y)} by A4, FUNCT_1:60; then A17: ( ex_sup_of {z,y},L implies ex_sup_of f .: {z,y}, BoolePoset {x} ) by YELLOW_0:20; A18: now__::_thesis:_(f_._z)_"\/"_(f_._y)_=_f_._(z_"\/"_y) percases ( ( f . z = {} & f . y = {} ) or ( f . z = {x} & f . y = {x} ) or ( f . z = {} & f . y = {x} ) or ( f . z = {x} & f . y = {} ) ) by A3, TARSKI:def_2; supposeA19: ( f . z = {} & f . y = {} ) ; ::_thesis: (f . z) "\/" (f . y) = f . (z "\/" y) then ( z <= l & y <= l ) by A2; then A20: z "\/" y <= l by YELLOW_0:22; thus (f . z) "\/" (f . y) = {} \/ {} by A19, YELLOW_1:17 .= f . (z "\/" y) by A2, A20 ; ::_thesis: verum end; supposeA21: ( f . z = {x} & f . y = {x} ) ; ::_thesis: (f . z) "\/" (f . y) = f . (z "\/" y) then ( z "\/" y >= z & not z <= l ) by A2, YELLOW_0:22; then not z "\/" y <= l by ORDERS_2:3; then A22: not f . (z "\/" y) = {} by A2; thus (f . z) "\/" (f . y) = {x} \/ {x} by A21, YELLOW_1:17 .= f . (z "\/" y) by A3, A22, TARSKI:def_2 ; ::_thesis: verum end; supposeA23: ( f . z = {} & f . y = {x} ) ; ::_thesis: (f . z) "\/" (f . y) = f . (z "\/" y) then ( z "\/" y >= y & not y <= l ) by A2, YELLOW_0:22; then not z "\/" y <= l by ORDERS_2:3; then A24: not f . (z "\/" y) = {} by A2; thus (f . z) "\/" (f . y) = {} \/ {x} by A23, YELLOW_1:17 .= f . (z "\/" y) by A3, A24, TARSKI:def_2 ; ::_thesis: verum end; supposeA25: ( f . z = {x} & f . y = {} ) ; ::_thesis: (f . z) "\/" (f . y) = f . (z "\/" y) then ( z "\/" y >= z & not z <= l ) by A2, YELLOW_0:22; then not z "\/" y <= l by ORDERS_2:3; then A26: not f . (z "\/" y) = {} by A2; thus (f . z) "\/" (f . y) = {x} \/ {} by A25, YELLOW_1:17 .= f . (z "\/" y) by A3, A26, TARSKI:def_2 ; ::_thesis: verum end; end; end; sup (f .: {z,y}) = (f . z) "\/" (f . y) by A16, YELLOW_0:41 .= f . (sup {z,y}) by A18, YELLOW_0:41 ; hence f preserves_sup_of {z,y} by A17, WAYBEL_0:def_31; ::_thesis: verum end; hence f is join-preserving by WAYBEL_0:def_35; ::_thesis: verum end; thus ( ( for x being set for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds ( f . p = {} iff p <= l ) ) holds ( f is meet-preserving & f is join-preserving ) ) implies l is prime ) ::_thesis: verum proof defpred S1[ Element of L, set ] means ( $1 <= l iff $2 = {} ); assume A27: for x being set for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds ( f . p = {} iff p <= l ) ) holds ( f is meet-preserving & f is join-preserving ) ; ::_thesis: l is prime let z, y be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not z "/\" y <= l or z <= l or y <= l ) A28: the carrier of (BoolePoset {{}}) = the carrier of (InclPoset (bool {{}})) by YELLOW_1:4 .= bool {{}} by YELLOW_1:1 .= {{},{{}}} by ZFMISC_1:24 ; A29: for a being Element of L ex b being Element of (BoolePoset {{}}) st S1[a,b] proof let a be Element of L; ::_thesis: ex b being Element of (BoolePoset {{}}) st S1[a,b] now__::_thesis:_ex_b_being_Element_of_(BoolePoset_{{}})_st_S1[a,b] percases ( a <= l or not a <= l ) ; supposeA30: a <= l ; ::_thesis: ex b being Element of (BoolePoset {{}}) st S1[a,b] set b = {} ; reconsider b = {} as Element of (BoolePoset {{}}) by A28, TARSKI:def_2; ( a <= l iff b = {} ) by A30; hence ex b being Element of (BoolePoset {{}}) st S1[a,b] ; ::_thesis: verum end; supposeA31: not a <= l ; ::_thesis: ex b being Element of (BoolePoset {{}}) st S1[a,b] set b = {{}}; reconsider b = {{}} as Element of (BoolePoset {{}}) by A28, TARSKI:def_2; ( a <= l iff b = {} ) by A31; hence ex b being Element of (BoolePoset {{}}) st S1[a,b] ; ::_thesis: verum end; end; end; hence ex b being Element of (BoolePoset {{}}) st S1[a,b] ; ::_thesis: verum end; consider f being Function of L,(BoolePoset {{}}) such that A32: for p being Element of L holds S1[p,f . p] from FUNCT_2:sch_3(A29); f is meet-preserving by A27, A32; then A33: ( ex_inf_of {z,y},L & f preserves_inf_of {z,y} ) by WAYBEL_0:def_34, YELLOW_0:21; dom f = the carrier of L by FUNCT_2:def_1; then A34: f .: {z,y} = {(f . z),(f . y)} by FUNCT_1:60; assume z "/\" y <= l ; ::_thesis: ( z <= l or y <= l ) then A35: {} = f . (z "/\" y) by A32 .= f . (inf {z,y}) by YELLOW_0:40 .= inf {(f . z),(f . y)} by A34, A33, WAYBEL_0:def_30 .= (f . z) "/\" (f . y) by YELLOW_0:40 .= (f . z) /\ (f . y) by YELLOW_1:17 ; now__::_thesis:_(_not_f_._z_=_{}_implies_f_._y_=_{}_) assume ( not f . z = {} & not f . y = {} ) ; ::_thesis: contradiction then ( f . z = {{}} & f . y = {{}} ) by A28, TARSKI:def_2; hence contradiction by A35; ::_thesis: verum end; hence ( z <= l or y <= l ) by A32; ::_thesis: verum end; end; theorem Th26: :: WAYBEL_6:26 for L being upper-bounded LATTICE for l being Element of L st l <> Top L holds ( l is prime iff (downarrow l) ` is Filter of L ) proof let L be upper-bounded LATTICE; ::_thesis: for l being Element of L st l <> Top L holds ( l is prime iff (downarrow l) ` is Filter of L ) let l be Element of L; ::_thesis: ( l <> Top L implies ( l is prime iff (downarrow l) ` is Filter of L ) ) set X1 = the carrier of L \ (downarrow l); reconsider X = the carrier of L \ (downarrow l) as Subset of L ; assume A1: l <> Top L ; ::_thesis: ( l is prime iff (downarrow l) ` is Filter of L ) thus ( l is prime implies (downarrow l) ` is Filter of L ) ::_thesis: ( (downarrow l) ` is Filter of L implies l is prime ) proof assume A2: l is prime ; ::_thesis: (downarrow l) ` is Filter of L A3: now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_X_&_y_in_X_holds_ ex_z_being_Element_of_L_st_ (_z_in_X_&_z_<=_x_&_z_<=_y_) let x, y be Element of L; ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & z <= x & z <= y ) ) assume that A4: x in X and A5: y in X ; ::_thesis: ex z being Element of L st ( z in X & z <= x & z <= y ) not y in downarrow l by A5, XBOOLE_0:def_5; then A6: not y <= l by WAYBEL_0:17; not x in downarrow l by A4, XBOOLE_0:def_5; then A7: not x <= l by WAYBEL_0:17; now__::_thesis:_not_x_"/\"_y_in_downarrow_l assume x "/\" y in downarrow l ; ::_thesis: contradiction then x "/\" y <= l by WAYBEL_0:17; hence contradiction by A2, A7, A6, Def6; ::_thesis: verum end; then A8: x "/\" y in X by XBOOLE_0:def_5; ( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23; hence ex z being Element of L st ( z in X & z <= x & z <= y ) by A8; ::_thesis: verum end; A9: now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_X_&_x_<=_y_holds_ y_in_X let x, y be Element of L; ::_thesis: ( x in X & x <= y implies y in X ) assume that A10: x in X and A11: x <= y ; ::_thesis: y in X not x in downarrow l by A10, XBOOLE_0:def_5; then not x <= l by WAYBEL_0:17; then not y <= l by A11, ORDERS_2:3; then not y in downarrow l by WAYBEL_0:17; hence y in X by XBOOLE_0:def_5; ::_thesis: verum end; now__::_thesis:_not_Top_L_in_downarrow_l assume Top L in downarrow l ; ::_thesis: contradiction then Top L <= l by WAYBEL_0:17; then Top L < l by A1, ORDERS_2:def_6; hence contradiction by ORDERS_2:6, YELLOW_0:45; ::_thesis: verum end; hence (downarrow l) ` is Filter of L by A3, A9, WAYBEL_0:def_2, WAYBEL_0:def_20, XBOOLE_0:def_5; ::_thesis: verum end; thus ( (downarrow l) ` is Filter of L implies l is prime ) ::_thesis: verum proof l <= l ; then A12: l in downarrow l by WAYBEL_0:17; assume A13: (downarrow l) ` is Filter of L ; ::_thesis: l is prime let x, y be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not x "/\" y <= l or x <= l or y <= l ) assume A14: x "/\" y <= l ; ::_thesis: ( x <= l or y <= l ) now__::_thesis:_(_not_x_<=_l_implies_y_<=_l_) assume that A15: not x <= l and A16: not y <= l ; ::_thesis: contradiction not y in downarrow l by A16, WAYBEL_0:17; then A17: y in X by XBOOLE_0:def_5; not x in downarrow l by A15, WAYBEL_0:17; then x in X by XBOOLE_0:def_5; then consider z being Element of L such that A18: z in X and A19: ( z <= x & z <= y ) by A13, A17, WAYBEL_0:def_2; z <= x "/\" y by A19, YELLOW_0:23; then z <= l by A14, ORDERS_2:3; then l in X by A13, A18, WAYBEL_0:def_20; hence contradiction by A12, XBOOLE_0:def_5; ::_thesis: verum end; hence ( x <= l or y <= l ) ; ::_thesis: verum end; end; theorem Th27: :: WAYBEL_6:27 for L being distributive LATTICE for l being Element of L holds ( l is prime iff l is irreducible ) proof let L be distributive LATTICE; ::_thesis: for l being Element of L holds ( l is prime iff l is irreducible ) let l be Element of L; ::_thesis: ( l is prime iff l is irreducible ) thus ( l is prime implies l is irreducible ) by Th24; ::_thesis: ( l is irreducible implies l is prime ) thus ( l is irreducible implies l is prime ) ::_thesis: verum proof assume A1: l is irreducible ; ::_thesis: l is prime let x, y be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not x "/\" y <= l or x <= l or y <= l ) assume x "/\" y <= l ; ::_thesis: ( x <= l or y <= l ) then l = l "\/" (x "/\" y) by YELLOW_0:24 .= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:5 ; then ( l = l "\/" x or l = l "\/" y ) by A1, Def2; hence ( x <= l or y <= l ) by YELLOW_0:24; ::_thesis: verum end; end; theorem Th28: :: WAYBEL_6:28 for L being distributive LATTICE holds PRIME L = IRR L proof let L be distributive LATTICE; ::_thesis: PRIME L = IRR L now__::_thesis:_for_l1_being_set_st_l1_in_PRIME_L_holds_ l1_in_IRR_L let l1 be set ; ::_thesis: ( l1 in PRIME L implies l1 in IRR L ) assume A1: l1 in PRIME L ; ::_thesis: l1 in IRR L then reconsider l = l1 as Element of PRIME L ; reconsider l = l as Element of L by A1; l is prime by A1, Def7; then l is irreducible by Th27; hence l1 in IRR L by Def4; ::_thesis: verum end; hence PRIME L c= IRR L by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: IRR L c= PRIME L now__::_thesis:_for_l1_being_set_st_l1_in_IRR_L_holds_ l1_in_PRIME_L let l1 be set ; ::_thesis: ( l1 in IRR L implies l1 in PRIME L ) assume A2: l1 in IRR L ; ::_thesis: l1 in PRIME L then reconsider l = l1 as Element of IRR L ; reconsider l = l as Element of L by A2; l is irreducible by A2, Def4; then l is prime by Th27; hence l1 in PRIME L by Def7; ::_thesis: verum end; hence IRR L c= PRIME L by TARSKI:def_3; ::_thesis: verum end; theorem :: WAYBEL_6:29 for L being Boolean LATTICE for l being Element of L st l <> Top L holds ( l is prime iff for x being Element of L st x > l holds x = Top L ) proof let L be Boolean LATTICE; ::_thesis: for l being Element of L st l <> Top L holds ( l is prime iff for x being Element of L st x > l holds x = Top L ) let l be Element of L; ::_thesis: ( l <> Top L implies ( l is prime iff for x being Element of L st x > l holds x = Top L ) ) assume A1: l <> Top L ; ::_thesis: ( l is prime iff for x being Element of L st x > l holds x = Top L ) thus ( l is prime implies for x being Element of L st x > l holds x = Top L ) ::_thesis: ( ( for x being Element of L st x > l holds x = Top L ) implies l is prime ) proof assume A2: l is prime ; ::_thesis: for x being Element of L st x > l holds x = Top L let x be Element of L; ::_thesis: ( x > l implies x = Top L ) consider y being Element of L such that A3: y is_a_complement_of x by WAYBEL_1:def_24; x "/\" y = Bottom L by A3, WAYBEL_1:def_23; then x "/\" y <= l by YELLOW_0:44; then A4: ( x <= l or y <= l ) by A2, Def6; assume x > l ; ::_thesis: x = Top L then y < x by A4, ORDERS_2:7; then A5: y <= x by ORDERS_2:def_6; x "\/" y = Top L by A3, WAYBEL_1:def_23; hence x = Top L by A5, YELLOW_0:24; ::_thesis: verum end; thus ( ( for x being Element of L st x > l holds x = Top L ) implies l is prime ) ::_thesis: verum proof assume A6: for z being Element of L st z > l holds z = Top L ; ::_thesis: l is prime let x, y be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not x "/\" y <= l or x <= l or y <= l ) assume x "/\" y <= l ; ::_thesis: ( x <= l or y <= l ) then A7: l = l "\/" (x "/\" y) by YELLOW_0:24 .= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:5 ; assume that A8: not x <= l and A9: not y <= l ; ::_thesis: contradiction A10: l <> l "\/" y by A9, YELLOW_0:24; l <= l "\/" y by A7, YELLOW_0:23; then l < l "\/" y by A10, ORDERS_2:def_6; then A11: l "\/" y = Top L by A6; A12: l <> l "\/" x by A8, YELLOW_0:24; l <= l "\/" x by A7, YELLOW_0:23; then l < l "\/" x by A12, ORDERS_2:def_6; then l "\/" x = Top L by A6; hence contradiction by A1, A7, A11, YELLOW_5:2; ::_thesis: verum end; end; theorem :: WAYBEL_6:30 for L being lower-bounded distributive continuous LATTICE for l being Element of L st l <> Top L holds ( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` ) proof let L be lower-bounded distributive continuous LATTICE; ::_thesis: for l being Element of L st l <> Top L holds ( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` ) let l be Element of L; ::_thesis: ( l <> Top L implies ( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` ) ) set F = (downarrow l) ` ; assume A1: l <> Top L ; ::_thesis: ( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` ) thus ( l is prime implies ex F being Open Filter of L st l is_maximal_in F ` ) ::_thesis: ( ex F being Open Filter of L st l is_maximal_in F ` implies l is prime ) proof A2: for x being Element of L holds ( not waybelow x is empty & waybelow x is directed ) ; A3: now__::_thesis:_for_x_being_Element_of_L_st_x_in_(downarrow_l)_`_holds_ ex_y_being_Element_of_L_st_ (_y_in_(downarrow_l)_`_&_y_<<_x_) let x be Element of L; ::_thesis: ( x in (downarrow l) ` implies ex y being Element of L st ( y in (downarrow l) ` & y << x ) ) assume x in (downarrow l) ` ; ::_thesis: ex y being Element of L st ( y in (downarrow l) ` & y << x ) then not x in downarrow l by XBOOLE_0:def_5; then not x <= l by WAYBEL_0:17; then consider y being Element of L such that A4: y << x and A5: not y <= l by A2, WAYBEL_3:24; not y in downarrow l by A5, WAYBEL_0:17; then y in (downarrow l) ` by XBOOLE_0:def_5; hence ex y being Element of L st ( y in (downarrow l) ` & y << x ) by A4; ::_thesis: verum end; assume l is prime ; ::_thesis: ex F being Open Filter of L st l is_maximal_in F ` then reconsider F = (downarrow l) ` as Open Filter of L by A1, A3, Def1, Th26; take F ; ::_thesis: l is_maximal_in F ` A6: now__::_thesis:_for_y_being_Element_of_L_holds_ (_not_y_in_F_`_or_not_y_>_l_) given y being Element of L such that A7: y in F ` and A8: y > l ; ::_thesis: contradiction y <= l by A7, WAYBEL_0:17; hence contradiction by A8, ORDERS_2:6; ::_thesis: verum end; l <= l ; then l in F ` by WAYBEL_0:17; hence l is_maximal_in F ` by A6, WAYBEL_4:55; ::_thesis: verum end; thus ( ex F being Open Filter of L st l is_maximal_in F ` implies l is prime ) ::_thesis: verum proof assume ex O being Open Filter of L st l is_maximal_in O ` ; ::_thesis: l is prime then A9: l is irreducible by Th13; now__::_thesis:_for_x,_y_being_Element_of_L_st_x_"/\"_y_<=_l_&_not_x_<=_l_holds_ y_<=_l let x, y be Element of L; ::_thesis: ( x "/\" y <= l & not x <= l implies y <= l ) assume x "/\" y <= l ; ::_thesis: ( not x <= l implies y <= l ) then l = l "\/" (x "/\" y) by YELLOW_0:24 .= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:5 ; then A10: ( l = l "\/" x or l = l "\/" y ) by A9, Def2; assume ( not x <= l & not y <= l ) ; ::_thesis: contradiction hence contradiction by A10, YELLOW_0:24; ::_thesis: verum end; hence l is prime by Def6; ::_thesis: verum end; end; theorem Th31: :: WAYBEL_6:31 for L being RelStr for X being Subset of L holds chi (X, the carrier of L) is Function of L,(BoolePoset {{}}) proof let L be RelStr ; ::_thesis: for X being Subset of L holds chi (X, the carrier of L) is Function of L,(BoolePoset {{}}) let X be Subset of L; ::_thesis: chi (X, the carrier of L) is Function of L,(BoolePoset {{}}) the carrier of (BoolePoset {{}}) = the carrier of (InclPoset (bool {{}})) by YELLOW_1:4 .= bool {{}} by YELLOW_1:1 .= {0,1} by CARD_1:49, ZFMISC_1:24 ; hence chi (X, the carrier of L) is Function of L,(BoolePoset {{}}) ; ::_thesis: verum end; theorem Th32: :: WAYBEL_6:32 for L being non empty RelStr for p, x being Element of L holds ( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p ) proof let L be non empty RelStr ; ::_thesis: for p, x being Element of L holds ( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p ) let p, x be Element of L; ::_thesis: ( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p ) ( not x in (downarrow p) ` iff x in downarrow p ) by XBOOLE_0:def_5; hence ( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p ) by FUNCT_3:def_3, WAYBEL_0:17; ::_thesis: verum end; theorem Th33: :: WAYBEL_6:33 for L being upper-bounded LATTICE for f being Function of L,(BoolePoset {{}}) for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds ( f is meet-preserving & f is join-preserving ) proof let L be upper-bounded LATTICE; ::_thesis: for f being Function of L,(BoolePoset {{}}) for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds ( f is meet-preserving & f is join-preserving ) let f be Function of L,(BoolePoset {{}}); ::_thesis: for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds ( f is meet-preserving & f is join-preserving ) let p be prime Element of L; ::_thesis: ( chi (((downarrow p) `), the carrier of L) = f implies ( f is meet-preserving & f is join-preserving ) ) assume chi (((downarrow p) `), the carrier of L) = f ; ::_thesis: ( f is meet-preserving & f is join-preserving ) then for x being Element of L holds ( f . x = {} iff x <= p ) by Th32; hence ( f is meet-preserving & f is join-preserving ) by Th25; ::_thesis: verum end; theorem Th34: :: WAYBEL_6:34 for L being complete LATTICE st PRIME L is order-generating holds ( L is distributive & L is meet-continuous ) proof let L be complete LATTICE; ::_thesis: ( PRIME L is order-generating implies ( L is distributive & L is meet-continuous ) ) set H = { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ; set p9 = the prime Element of L; A1: chi (((downarrow the prime Element of L) `), the carrier of L) in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ; now__::_thesis:_for_x_being_set_st_x_in__{__(chi_(((downarrow_p)_`),_the_carrier_of_L))_where_p_is_Element_of_L_:_p_is_prime__}__holds_ x_is_Function let x be set ; ::_thesis: ( x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } implies x is Function ) assume x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ; ::_thesis: x is Function then ex p being Element of L st ( x = chi (((downarrow p) `), the carrier of L) & p is prime ) ; hence x is Function ; ::_thesis: verum end; then reconsider H = { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } as non empty functional set by A1, FUNCT_1:def_13; deffunc H1( set ) -> set = { f where f is Element of H : f . $1 = 1 } ; consider F being Function such that A2: dom F = the carrier of L and A3: for x being set st x in the carrier of L holds F . x = H1(x) from FUNCT_1:sch_3(); A4: the carrier of (BoolePoset H) = the carrier of (InclPoset (bool H)) by YELLOW_1:4 .= bool H by YELLOW_1:1 ; rng F c= the carrier of (BoolePoset H) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in the carrier of (BoolePoset H) ) assume y in rng F ; ::_thesis: y in the carrier of (BoolePoset H) then consider x being set such that A5: ( x in dom F & y = F . x ) by FUNCT_1:def_3; A6: y = { f where f is Element of H : f . x = 1 } by A2, A3, A5; y c= H proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in y or p in H ) assume p in y ; ::_thesis: p in H then ex f being Element of H st ( p = f & f . x = 1 ) by A6; hence p in H ; ::_thesis: verum end; hence y in the carrier of (BoolePoset H) by A4; ::_thesis: verum end; then reconsider F = F as Function of L,(BoolePoset H) by A2, FUNCT_2:def_1, RELSET_1:4; A7: F is meet-preserving proof let x, y be Element of L; :: according to WAYBEL_0:def_34 ::_thesis: F preserves_inf_of {x,y} assume ex_inf_of {x,y},L ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of F .: {x,y}, BoolePoset H & "/\" ((F .: {x,y}),(BoolePoset H)) = F . ("/\" ({x,y},L)) ) thus ex_inf_of F .: {x,y}, BoolePoset H by YELLOW_0:17; ::_thesis: "/\" ((F .: {x,y}),(BoolePoset H)) = F . ("/\" ({x,y},L)) A8: { f where f is Element of H : f . (x "/\" y) = 1 } c= { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } proof A9: ( ex_inf_of {x,y},L & x "/\" y = inf {x,y} ) by YELLOW_0:17, YELLOW_0:40; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { f where f is Element of H : f . (x "/\" y) = 1 } or p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } ) A10: 1 = Top (BoolePoset {{}}) by CARD_1:49, YELLOW_1:19; assume p in { f where f is Element of H : f . (x "/\" y) = 1 } ; ::_thesis: p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } then consider g being Element of H such that A11: g = p and A12: g . (x "/\" y) = 1 ; g in H ; then A13: ex a being Element of L st ( chi (((downarrow a) `), the carrier of L) = g & a is prime ) ; then reconsider g = g as Function of L,(BoolePoset {{}}) by Th31; g is meet-preserving by A13, Th33; then A14: g preserves_inf_of {x,y} by WAYBEL_0:def_34; dom g = the carrier of L by FUNCT_2:def_1; then A15: {(g . x),(g . y)} = g .: {x,y} by FUNCT_1:60; (g . x) "/\" (g . y) = inf {(g . x),(g . y)} by YELLOW_0:40; then A16: g . (x "/\" y) = (g . x) "/\" (g . y) by A15, A14, A9, WAYBEL_0:def_30; then ( g . y <= Top (BoolePoset {{}}) & g . y >= Top (BoolePoset {{}}) ) by A12, A10, YELLOW_0:23, YELLOW_0:45; then g . y = 1 by A10, ORDERS_2:2; then A17: p in { f where f is Element of H : f . y = 1 } by A11; ( g . x <= Top (BoolePoset {{}}) & g . x >= Top (BoolePoset {{}}) ) by A12, A10, A16, YELLOW_0:23, YELLOW_0:45; then g . x = 1 by A10, ORDERS_2:2; then p in { f where f is Element of H : f . x = 1 } by A11; hence p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } by A17, XBOOLE_0:def_4; ::_thesis: verum end; A18: { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } c= { f where f is Element of H : f . (x "/\" y) = 1 } proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } or p in { f where f is Element of H : f . (x "/\" y) = 1 } ) A19: ( ex_inf_of {x,y},L & x "/\" y = inf {x,y} ) by YELLOW_0:17, YELLOW_0:40; assume A20: p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } ; ::_thesis: p in { f where f is Element of H : f . (x "/\" y) = 1 } then p in { f where f is Element of H : f . x = 1 } by XBOOLE_0:def_4; then consider f1 being Element of H such that A21: f1 = p and A22: f1 . x = 1 ; p in { f where f is Element of H : f . y = 1 } by A20, XBOOLE_0:def_4; then A23: ex f2 being Element of H st ( f2 = p & f2 . y = 1 ) ; f1 in H ; then consider a being Element of L such that A24: chi (((downarrow a) `), the carrier of L) = f1 and A25: a is prime ; reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A24, Th31; for x being Element of L holds ( f1 . x = {} iff x <= a ) by A24, Th32; then f1 is meet-preserving by A25, Th25; then A26: f1 preserves_inf_of {x,y} by WAYBEL_0:def_34; dom f1 = the carrier of L by FUNCT_2:def_1; then A27: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60; (f1 . x) "/\" (f1 . y) = inf {(f1 . x),(f1 . y)} by YELLOW_0:40; then f1 . (x "/\" y) = (f1 . x) "/\" (f1 . y) by A27, A26, A19, WAYBEL_0:def_30 .= 1 by A21, A22, A23, YELLOW_5:2 ; hence p in { f where f is Element of H : f . (x "/\" y) = 1 } by A21; ::_thesis: verum end; F .: {x,y} = {(F . x),(F . y)} by A2, FUNCT_1:60; hence inf (F .: {x,y}) = (F . x) "/\" (F . y) by YELLOW_0:40 .= (F . x) /\ (F . y) by YELLOW_1:17 .= { f where f is Element of H : f . x = 1 } /\ (F . y) by A3 .= { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } by A3 .= { f where f is Element of H : f . (x "/\" y) = 1 } by A18, A8, XBOOLE_0:def_10 .= F . (x "/\" y) by A3 .= F . (inf {x,y}) by YELLOW_0:40 ; ::_thesis: verum end; assume A28: PRIME L is order-generating ; ::_thesis: ( L is distributive & L is meet-continuous ) A29: F is V24() proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 ) assume that A30: x1 in dom F and A31: x2 in dom F and A32: F . x1 = F . x2 ; ::_thesis: x1 = x2 reconsider l2 = x2 as Element of L by A31; reconsider l1 = x1 as Element of L by A30; now__::_thesis:_not_l1_<>_l2 A33: F . l2 = { f where f is Element of H : f . l2 = 1 } by A3; A34: F . l1 = { f where f is Element of H : f . l1 = 1 } by A3; assume A35: l1 <> l2 ; ::_thesis: contradiction percases ( not l1 <= l2 or not l2 <= l1 ) by A35, ORDERS_2:2; suppose not l1 <= l2 ; ::_thesis: contradiction then consider p being Element of L such that A36: p in PRIME L and A37: l2 <= p and A38: not l1 <= p by A28, Th17; set CH = chi (((downarrow p) `), the carrier of L); p is prime by A36, Def7; then chi (((downarrow p) `), the carrier of L) in H ; then reconsider CH = chi (((downarrow p) `), the carrier of L) as Element of H ; A39: now__::_thesis:_not_CH_in_F_._l2 assume CH in F . l2 ; ::_thesis: contradiction then ex f being Element of H st ( f = CH & f . l2 = 1 ) by A33; hence contradiction by A37, Th32; ::_thesis: verum end; dom CH = the carrier of L by FUNCT_2:def_1; then ( rng CH c= {0,1} & CH . l1 in rng CH ) by FUNCT_1:def_3, RELAT_1:def_19; then ( CH . l1 = 0 or CH . l1 = 1 ) by TARSKI:def_2; hence contradiction by A32, A34, A38, A39, Th32; ::_thesis: verum end; suppose not l2 <= l1 ; ::_thesis: contradiction then consider p being Element of L such that A40: p in PRIME L and A41: l1 <= p and A42: not l2 <= p by A28, Th17; set CH = chi (((downarrow p) `), the carrier of L); p is prime by A40, Def7; then chi (((downarrow p) `), the carrier of L) in H ; then reconsider CH = chi (((downarrow p) `), the carrier of L) as Element of H ; A43: now__::_thesis:_not_CH_in_F_._l1 assume CH in F . l1 ; ::_thesis: contradiction then ex f being Element of H st ( f = CH & f . l1 = 1 ) by A34; hence contradiction by A41, Th32; ::_thesis: verum end; dom CH = the carrier of L by FUNCT_2:def_1; then ( rng CH c= {0,1} & CH . l2 in rng CH ) by FUNCT_1:def_3, RELAT_1:def_19; then ( CH . l2 = 0 or CH . l2 = 1 ) by TARSKI:def_2; hence contradiction by A32, A33, A42, A43, Th32; ::_thesis: verum end; end; end; hence x1 = x2 ; ::_thesis: verum end; F is join-preserving proof let x, y be Element of L; :: according to WAYBEL_0:def_35 ::_thesis: F preserves_sup_of {x,y} assume ex_sup_of {x,y},L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of F .: {x,y}, BoolePoset H & "\/" ((F .: {x,y}),(BoolePoset H)) = F . ("\/" ({x,y},L)) ) thus ex_sup_of F .: {x,y}, BoolePoset H by YELLOW_0:17; ::_thesis: "\/" ((F .: {x,y}),(BoolePoset H)) = F . ("\/" ({x,y},L)) A44: { f where f is Element of H : f . (x "\/" y) = 1 } c= { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { f where f is Element of H : f . (x "\/" y) = 1 } or p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } ) A45: 1 = Top (BoolePoset {{}}) by CARD_1:49, YELLOW_1:19; assume p in { f where f is Element of H : f . (x "\/" y) = 1 } ; ::_thesis: p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } then consider g being Element of H such that A46: g = p and A47: g . (x "\/" y) = 1 ; g in H ; then A48: ex a being Element of L st ( chi (((downarrow a) `), the carrier of L) = g & a is prime ) ; then reconsider g = g as Function of L,(BoolePoset {{}}) by Th31; g is join-preserving by A48, Th33; then A49: g preserves_sup_of {x,y} by WAYBEL_0:def_35; dom g = the carrier of L by FUNCT_2:def_1; then A50: g .: {x,y} = {(g . x),(g . y)} by FUNCT_1:60; A51: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41; A52: (g . x) "\/" (g . y) = sup {(g . x),(g . y)} by YELLOW_0:41; A53: now__::_thesis:_(_g_._x_=_{}_implies_not_g_._y_=_{}_) assume ( g . x = {} & g . y = {} ) ; ::_thesis: contradiction then (g . x) "\/" (g . y) = {} \/ {} by YELLOW_1:17 .= 0 ; hence contradiction by A47, A50, A49, A51, A52, WAYBEL_0:def_31; ::_thesis: verum end; A54: the carrier of (BoolePoset {{}}) = the carrier of (InclPoset (bool {{}})) by YELLOW_1:4 .= bool {{}} by YELLOW_1:1 .= {{},{{}}} by ZFMISC_1:24 ; then A55: ( g . y = {} or g . y = {{}} ) by TARSKI:def_2; ( g . x = {} or g . x = {{}} ) by A54, TARSKI:def_2; then ( g . x = Top (BoolePoset {{}}) or g . y = Top (BoolePoset {{}}) ) by A55, A53, YELLOW_1:19; then ( p in { f where f is Element of H : f . x = 1 } or p in { f where f is Element of H : f . y = 1 } ) by A46, A45; hence p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } by XBOOLE_0:def_3; ::_thesis: verum end; A56: { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } c= { f where f is Element of H : f . (x "\/" y) = 1 } proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } or p in { f where f is Element of H : f . (x "\/" y) = 1 } ) assume A57: p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } ; ::_thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 } percases ( p in { f where f is Element of H : f . x = 1 } or p in { f where f is Element of H : f . y = 1 } ) by A57, XBOOLE_0:def_3; suppose p in { f where f is Element of H : f . x = 1 } ; ::_thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 } then consider f1 being Element of H such that A58: f1 = p and A59: f1 . x = 1 ; f1 in H ; then consider a being Element of L such that A60: chi (((downarrow a) `), the carrier of L) = f1 and A61: a is prime ; reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A60, Th31; for x being Element of L holds ( f1 . x = {} iff x <= a ) by A60, Th32; then f1 is join-preserving by A61, Th25; then A62: f1 preserves_sup_of {x,y} by WAYBEL_0:def_35; dom f1 = the carrier of L by FUNCT_2:def_1; then A63: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60; A64: ( 1 = Top (BoolePoset {{}}) & f1 . y <= Top (BoolePoset {{}}) ) by CARD_1:49, YELLOW_0:45, YELLOW_1:19; A65: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41; (f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} by YELLOW_0:41; then f1 . (x "\/" y) = (f1 . x) "\/" (f1 . y) by A63, A62, A65, WAYBEL_0:def_31 .= 1 by A59, A64, YELLOW_0:24 ; hence p in { f where f is Element of H : f . (x "\/" y) = 1 } by A58; ::_thesis: verum end; suppose p in { f where f is Element of H : f . y = 1 } ; ::_thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 } then consider f1 being Element of H such that A66: f1 = p and A67: f1 . y = 1 ; f1 in H ; then consider b being Element of L such that A68: chi (((downarrow b) `), the carrier of L) = f1 and A69: b is prime ; reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A68, Th31; for x being Element of L holds ( f1 . x = {} iff x <= b ) by A68, Th32; then f1 is join-preserving by A69, Th25; then A70: f1 preserves_sup_of {x,y} by WAYBEL_0:def_35; dom f1 = the carrier of L by FUNCT_2:def_1; then A71: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60; A72: ( 1 = Top (BoolePoset {{}}) & f1 . x <= Top (BoolePoset {{}}) ) by CARD_1:49, YELLOW_0:45, YELLOW_1:19; A73: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41; (f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} by YELLOW_0:41; then f1 . (x "\/" y) = (f1 . y) "\/" (f1 . x) by A71, A70, A73, WAYBEL_0:def_31 .= 1 by A67, A72, YELLOW_0:24 ; hence p in { f where f is Element of H : f . (x "\/" y) = 1 } by A66; ::_thesis: verum end; end; end; F .: {x,y} = {(F . x),(F . y)} by A2, FUNCT_1:60; hence sup (F .: {x,y}) = (F . x) "\/" (F . y) by YELLOW_0:41 .= (F . x) \/ (F . y) by YELLOW_1:17 .= { f where f is Element of H : f . x = 1 } \/ (F . y) by A3 .= { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } by A3 .= { f where f is Element of H : f . (x "\/" y) = 1 } by A56, A44, XBOOLE_0:def_10 .= F . (x "\/" y) by A3 .= F . (sup {x,y}) by YELLOW_0:41 ; ::_thesis: verum end; hence L is distributive by A7, A29, Th3; ::_thesis: L is meet-continuous F is sups-preserving proof let X be Subset of L; :: according to WAYBEL_0:def_33 ::_thesis: F preserves_sup_of X F preserves_sup_of X proof assume ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of F .: X, BoolePoset H & "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L)) ) thus ex_sup_of F .: X, BoolePoset H by YELLOW_0:17; ::_thesis: "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L)) A74: F . (sup X) = { g where g is Element of H : g . (sup X) = 1 } by A3; A75: sup (F .: X) c= F . (sup X) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in sup (F .: X) or a in F . (sup X) ) assume a in sup (F .: X) ; ::_thesis: a in F . (sup X) then a in union (F .: X) by YELLOW_1:21; then consider Y being set such that A76: a in Y and A77: Y in F .: X by TARSKI:def_4; consider z being set such that A78: z in dom F and A79: z in X and A80: Y = F . z by A77, FUNCT_1:def_6; reconsider z = z as Element of L by A78; F . z = { f where f is Element of H : f . z = 1 } by A3; then consider f being Element of H such that A81: a = f and A82: f . z = 1 by A76, A80; f in H ; then consider p being Element of L such that A83: f = chi (((downarrow p) `), the carrier of L) and p is prime ; A84: now__::_thesis:_not_f_._(sup_X)_=_0 sup X is_>=_than X by YELLOW_0:32; then A85: z <= sup X by A79, LATTICE3:def_9; assume f . (sup X) = 0 ; ::_thesis: contradiction then sup X <= p by A83, Th32; then z <= p by A85, ORDERS_2:3; hence contradiction by A82, A83, Th32; ::_thesis: verum end; dom f = the carrier of L by A83, FUNCT_2:def_1; then A86: f . (sup X) in rng f by FUNCT_1:def_3; rng f c= {0,1} by A83, RELAT_1:def_19; then ( f . (sup X) = 0 or f . (sup X) = 1 ) by A86, TARSKI:def_2; hence a in F . (sup X) by A74, A81, A84; ::_thesis: verum end; F . (sup X) c= sup (F .: X) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in F . (sup X) or a in sup (F .: X) ) assume a in F . (sup X) ; ::_thesis: a in sup (F .: X) then consider f being Element of H such that A87: a = f and A88: f . (sup X) = 1 by A74; f in H ; then consider p being Element of L such that A89: f = chi (((downarrow p) `), the carrier of L) and p is prime ; A90: rng f c= {0,1} by A89, RELAT_1:def_19; A91: not sup X <= p by A88, A89, Th32; now__::_thesis:_ex_l_being_Element_of_L_st_ (_l_in_X_&_not_l_<=_p_) assume for l being Element of L st l in X holds l <= p ; ::_thesis: contradiction then X is_<=_than p by LATTICE3:def_9; hence contradiction by A91, YELLOW_0:32; ::_thesis: verum end; then consider l being Element of L such that A92: l in X and A93: not l <= p ; dom f = the carrier of L by A89, FUNCT_2:def_1; then f . l in rng f by FUNCT_1:def_3; then ( f . l = 0 or f . l = 1 ) by A90, TARSKI:def_2; then f in { g where g is Element of H : g . l = 1 } by A89, A93, Th32; then A94: f in F . l by A3; F . l in F .: X by A2, A92, FUNCT_1:def_6; then a in union (F .: X) by A87, A94, TARSKI:def_4; hence a in sup (F .: X) by YELLOW_1:21; ::_thesis: verum end; hence "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L)) by A75, XBOOLE_0:def_10; ::_thesis: verum end; hence F preserves_sup_of X ; ::_thesis: verum end; hence L is meet-continuous by A7, A29, Th4; ::_thesis: verum end; theorem Th35: :: WAYBEL_6:35 for L being lower-bounded continuous LATTICE holds ( L is distributive iff PRIME L is order-generating ) proof let L be lower-bounded continuous LATTICE; ::_thesis: ( L is distributive iff PRIME L is order-generating ) thus ( L is distributive implies PRIME L is order-generating ) ::_thesis: ( PRIME L is order-generating implies L is distributive ) proof assume L is distributive ; ::_thesis: PRIME L is order-generating then A1: PRIME L = IRR L by Th28; (IRR L) \ {(Top L)} c= IRR L by XBOOLE_1:36; hence PRIME L is order-generating by A1, Th18, Th19; ::_thesis: verum end; thus ( PRIME L is order-generating implies L is distributive ) by Th34; ::_thesis: verum end; theorem :: WAYBEL_6:36 for L being lower-bounded continuous LATTICE holds ( L is distributive iff L is Heyting ) proof let L be lower-bounded continuous LATTICE; ::_thesis: ( L is distributive iff L is Heyting ) thus ( L is distributive implies L is Heyting ) ::_thesis: ( L is Heyting implies L is distributive ) proof assume L is distributive ; ::_thesis: L is Heyting then PRIME L is order-generating by Th35; then ( L is distributive & L is meet-continuous ) by Th34; hence L is Heyting ; ::_thesis: verum end; thus ( L is Heyting implies L is distributive ) ; ::_thesis: verum end; theorem Th37: :: WAYBEL_6:37 for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) holds for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) proof let L be complete continuous LATTICE; ::_thesis: ( ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) implies for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) ) defpred S1[ set , set ] means ( $2 c= PRIME (L ~) & $1 = "\/" ($2,L) ); assume A1: for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ; ::_thesis: for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) A2: for e being set st e in the carrier of L holds ex u being set st S1[e,u] proof let e be set ; ::_thesis: ( e in the carrier of L implies ex u being set st S1[e,u] ) assume e in the carrier of L ; ::_thesis: ex u being set st S1[e,u] then reconsider l = e as Element of L ; consider X being Subset of L such that A3: l = sup X and A4: for x being Element of L st x in X holds x is co-prime by A1; now__::_thesis:_for_p1_being_set_st_p1_in_X_holds_ p1_in_PRIME_(L_~) let p1 be set ; ::_thesis: ( p1 in X implies p1 in PRIME (L ~) ) assume A5: p1 in X ; ::_thesis: p1 in PRIME (L ~) then reconsider p = p1 as Element of L ; p is co-prime by A4, A5; then p ~ is prime by Def8; hence p1 in PRIME (L ~) by Def7; ::_thesis: verum end; then X c= PRIME (L ~) by TARSKI:def_3; hence ex u being set st S1[e,u] by A3; ::_thesis: verum end; consider f being Function such that A6: dom f = the carrier of L and A7: for e being set st e in the carrier of L holds S1[e,f . e] from CLASSES1:sch_1(A2); let l be Element of L; ::_thesis: l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) A8: ex_sup_of (waybelow l) /\ (PRIME (L ~)),L by YELLOW_0:17; A9: waybelow l c= { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in waybelow l or e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ) assume A10: e in waybelow l ; ::_thesis: e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } then f . e c= PRIME (L ~) by A7; then A11: f . e c= the carrier of (L ~) by XBOOLE_1:1; ( e = "\/" ((f . e),L) & f . e in rng f ) by A6, A7, A10, FUNCT_1:def_3; hence e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } by A10, A11; ::_thesis: verum end; defpred S2[ Subset of L] means ( $1 in rng f & sup $1 in waybelow l ); A12: l = sup (waybelow l) by WAYBEL_3:def_5; set Z = union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ; A13: union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } c= (waybelow l) /\ (PRIME (L ~)) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } or e in (waybelow l) /\ (PRIME (L ~)) ) assume e in union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ; ::_thesis: e in (waybelow l) /\ (PRIME (L ~)) then consider Y being set such that A14: e in Y and A15: Y in { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } by TARSKI:def_4; consider X being Subset of L such that A16: Y = X and A17: X in rng f and A18: sup X in waybelow l by A15; reconsider e1 = e as Element of L by A14, A16; e1 <= sup X by A14, A16, YELLOW_2:22; then A19: e in waybelow l by A18, WAYBEL_0:def_19; ex r being set st ( r in dom f & X = f . r ) by A17, FUNCT_1:def_3; then X c= PRIME (L ~) by A6, A7; hence e in (waybelow l) /\ (PRIME (L ~)) by A14, A16, A19, XBOOLE_0:def_4; ::_thesis: verum end; A20: ex_sup_of union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ,L by YELLOW_0:17; ex_sup_of waybelow l,L by YELLOW_0:17; then A21: "\/" (((waybelow l) /\ (PRIME (L ~))),L) <= "\/" ((waybelow l),L) by A8, XBOOLE_1:17, YELLOW_0:34; { (sup X) where X is Subset of L : S2[X] } c= waybelow l proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (sup X) where X is Subset of L : S2[X] } or e in waybelow l ) assume e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ; ::_thesis: e in waybelow l then ex X being Subset of L st ( e = sup X & X in rng f & sup X in waybelow l ) ; hence e in waybelow l ; ::_thesis: verum end; then l = "\/" ( { (sup X) where X is Subset of L : S2[X] } ,L) by A12, A9, XBOOLE_0:def_10 .= "\/" ((union { X where X is Subset of L : S2[X] } ),L) from YELLOW_3:sch_5() ; then l <= "\/" (((waybelow l) /\ (PRIME (L ~))),L) by A20, A8, A13, YELLOW_0:34; hence l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) by A12, A21, ORDERS_2:2; ::_thesis: verum end; Lm2: for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) holds L is completely-distributive proof let L be complete continuous LATTICE; ::_thesis: ( ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) implies L is completely-distributive ) assume A1: for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ; ::_thesis: L is completely-distributive thus L is complete ; :: according to WAYBEL_5:def_3 ::_thesis: for b1 being set for b2 being set for b3 being ManySortedFunction of b2,b1 --> the carrier of L holds //\ ((\// (b3,L)),L) = \\/ ((/\\ ((Frege b3),L)),L) let J be non empty set ; ::_thesis: for b1 being set for b2 being ManySortedFunction of b1,J --> the carrier of L holds //\ ((\// (b2,L)),L) = \\/ ((/\\ ((Frege b2),L)),L) let K be V19() ManySortedSet of J; ::_thesis: for b1 being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b1,L)),L) = \\/ ((/\\ ((Frege b1),L)),L) let F be DoubleIndexedSet of K,L; ::_thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L) set l = Inf ; set X = (waybelow (Inf )) /\ (PRIME (L ~)); A2: (waybelow (Inf )) /\ (PRIME (L ~)) c= waybelow (Inf ) by XBOOLE_1:17; reconsider X = (waybelow (Inf )) /\ (PRIME (L ~)) as Subset of L ; A3: dom F = J by PARTFUN1:def_2; A4: for x being Element of L st x in X holds x is co-prime proof let x be Element of L; ::_thesis: ( x in X implies x is co-prime ) assume x in X ; ::_thesis: x is co-prime then x in PRIME (L ~) by XBOOLE_0:def_4; then x ~ is prime by Def7; hence x is co-prime by Def8; ::_thesis: verum end; A5: inf (rng (Sups )) = Inf by YELLOW_2:def_6; X is_<=_than Sup proof let p be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not p in X or p <= Sup ) defpred S1[ set , set ] means ( $2 in K . $1 & [p,((F . $1) . $2)] in the InternalRel of L ); assume A6: p in X ; ::_thesis: p <= Sup A7: for j being set st j in J holds ex k being set st S1[j,k] proof let j1 be set ; ::_thesis: ( j1 in J implies ex k being set st S1[j1,k] ) assume j1 in J ; ::_thesis: ex k being set st S1[j1,k] then reconsider j = j1 as Element of J ; set k = the Element of K . j; dom (Sups ) = J by A3, FUNCT_2:def_1; then A8: (Sups ) . j in rng (Sups ) by FUNCT_1:def_3; A9: ( p << Inf & Sup = sup (rng (F . j)) ) by A2, A6, WAYBEL_3:7, YELLOW_2:def_5; Sup = (Sups ) . j by A3, WAYBEL_5:def_1; then Inf <= Sup by A5, A8, YELLOW_2:22; then consider A being finite Subset of L such that A10: A c= rng (F . j) and A11: p <= sup A by A9, WAYBEL_3:18; ( ex_sup_of A,L & ex_sup_of A \/ {((F . j) . the Element of K . j)},L ) by YELLOW_0:17; then sup A <= sup (A \/ {((F . j) . the Element of K . j)}) by XBOOLE_1:7, YELLOW_0:34; then A12: p <= sup (A \/ {((F . j) . the Element of K . j)}) by A11, ORDERS_2:3; p is co-prime by A4, A6; then consider a being Element of L such that A13: a in A \/ {((F . j) . the Element of K . j)} and A14: p <= a by A12, Th23; percases ( a in A or a in {((F . j) . the Element of K . j)} ) by A13, XBOOLE_0:def_3; suppose a in A ; ::_thesis: ex k being set st S1[j1,k] then consider k1 being set such that A15: k1 in dom (F . j) and A16: a = (F . j) . k1 by A10, FUNCT_1:def_3; reconsider k1 = k1 as Element of K . j by A15; [p,((F . j) . k1)] in the InternalRel of L by A14, A16, ORDERS_2:def_5; hence ex k being set st S1[j1,k] ; ::_thesis: verum end; suppose a in {((F . j) . the Element of K . j)} ; ::_thesis: ex k being set st S1[j1,k] then a = (F . j) . the Element of K . j by TARSKI:def_1; then [p,((F . j) . the Element of K . j)] in the InternalRel of L by A14, ORDERS_2:def_5; hence ex k being set st S1[j1,k] ; ::_thesis: verum end; end; end; consider f1 being Function such that A17: dom f1 = J and A18: for j being set st j in J holds S1[j,f1 . j] from CLASSES1:sch_1(A7); now__::_thesis:_for_g_being_set_st_g_in_dom_(doms_F)_holds_ g_in_dom_f1 let g be set ; ::_thesis: ( g in dom (doms F) implies g in dom f1 ) assume g in dom (doms F) ; ::_thesis: g in dom f1 then g in F " (SubFuncs (rng F)) by FUNCT_6:def_2; hence g in dom f1 by A3, A17, FUNCT_6:19; ::_thesis: verum end; then A19: dom (doms F) c= dom f1 by TARSKI:def_3; now__::_thesis:_for_g_being_set_st_g_in_dom_f1_holds_ g_in_dom_(doms_F) let g be set ; ::_thesis: ( g in dom f1 implies g in dom (doms F) ) A20: F . g is Function ; assume g in dom f1 ; ::_thesis: g in dom (doms F) then g in F " (SubFuncs (rng F)) by A3, A17, A20, FUNCT_6:19; hence g in dom (doms F) by FUNCT_6:def_2; ::_thesis: verum end; then dom f1 c= dom (doms F) by TARSKI:def_3; then A21: dom f1 = dom (doms F) by A19, XBOOLE_0:def_10; A22: for b being set st b in dom (doms F) holds f1 . b in (doms F) . b proof let b be set ; ::_thesis: ( b in dom (doms F) implies f1 . b in (doms F) . b ) assume A23: b in dom (doms F) ; ::_thesis: f1 . b in (doms F) . b then A24: F . b is Function of (K . b), the carrier of L by A17, A19, WAYBEL_5:6; (doms F) . b = dom (F . b) by A3, A17, A19, A23, FUNCT_6:22 .= K . b by A24, FUNCT_2:def_1 ; hence f1 . b in (doms F) . b by A17, A18, A19, A23; ::_thesis: verum end; then reconsider D = product (doms F) as non empty set by A21, CARD_3:9; reconsider f = f1 as Element of product (doms F) by A21, A22, CARD_3:9; A25: f1 in product (doms F) by A21, A22, CARD_3:9; p is_<=_than rng ((Frege F) . f) proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in rng ((Frege F) . f) or p <= b ) assume b in rng ((Frege F) . f) ; ::_thesis: p <= b then consider a being set such that A26: a in dom ((Frege F) . f) and A27: b = ((Frege F) . f) . a by FUNCT_1:def_3; reconsider a = a as Element of J by A26; f in dom (Frege F) by A25, PARTFUN1:def_2; then ((Frege F) . f) . a = (F . a) . (f1 . a) by A3, WAYBEL_5:9; then [p,(((Frege F) . f) . a)] in the InternalRel of L by A18; hence p <= b by A27, ORDERS_2:def_5; ::_thesis: verum end; then p <= inf (rng ((Frege F) . f)) by YELLOW_0:33; then A28: p <= Inf by YELLOW_2:def_6; reconsider P = D --> J as ManySortedSet of D ; reconsider R = Frege F as DoubleIndexedSet of P,L ; reconsider f2 = f as Element of D ; Inf in rng (Infs ) by WAYBEL_5:14; then Inf <= sup (rng (Infs )) by YELLOW_2:22; then Inf <= Sup by YELLOW_2:def_5; hence p <= Sup by A28, ORDERS_2:3; ::_thesis: verum end; then A29: sup X <= Sup by YELLOW_0:32; ( Inf >= Sup & Inf = sup X ) by A1, Th37, WAYBEL_5:16; hence //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L) by A29, ORDERS_2:2; ::_thesis: verum end; Lm3: for L being complete completely-distributive LATTICE holds ( L is distributive & L is continuous & L ~ is continuous ) proof let L be complete completely-distributive LATTICE; ::_thesis: ( L is distributive & L is continuous & L ~ is continuous ) L ~ is completely-distributive by YELLOW_7:51; hence ( L is distributive & L is continuous & L ~ is continuous ) ; ::_thesis: verum end; Lm4: for L being complete LATTICE st L is distributive & L is continuous & L ~ is continuous holds for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) proof let L be complete LATTICE; ::_thesis: ( L is distributive & L is continuous & L ~ is continuous implies for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) assume that A1: ( L is distributive & L is continuous ) and A2: L ~ is continuous ; ::_thesis: for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) let l be Element of L; ::_thesis: ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) reconsider L = L as distributive complete continuous LATTICE by A1; reconsider l1 = l as Element of (L ~) ; PRIME (L ~) is order-generating by A2, Th35; then consider Y being Subset of (PRIME (L ~)) such that A3: l1 = "/\" (Y,(L ~)) by Th15; reconsider Y = Y as Subset of L by XBOOLE_1:1; A4: for x being Element of L st x in Y holds x is co-prime proof let x be Element of L; ::_thesis: ( x in Y implies x is co-prime ) assume x in Y ; ::_thesis: x is co-prime then x ~ is prime by Def7; hence x is co-prime by Def8; ::_thesis: verum end; ex_sup_of Y,L by YELLOW_0:17; then "\/" (Y,L) = "/\" (Y,(L ~)) by YELLOW_7:12; hence ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) by A3, A4; ::_thesis: verum end; theorem :: WAYBEL_6:38 for L being complete LATTICE holds ( L is completely-distributive iff ( L is continuous & ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) ) ) proof let L be complete LATTICE; ::_thesis: ( L is completely-distributive iff ( L is continuous & ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) ) ) thus ( L is completely-distributive implies ( L is continuous & ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) ) ) ::_thesis: ( L is continuous & ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) implies L is completely-distributive ) proof assume L is completely-distributive ; ::_thesis: ( L is continuous & ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) ) then reconsider L = L as completely-distributive LATTICE ; L ~ is continuous by Lm3; hence ( L is continuous & ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) ) by Lm4; ::_thesis: verum end; thus ( L is continuous & ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) implies L is completely-distributive ) by Lm2; ::_thesis: verum end; theorem :: WAYBEL_6:39 for L being complete LATTICE holds ( L is completely-distributive iff ( L is distributive & L is continuous & L opp is continuous ) ) proof let L be complete LATTICE; ::_thesis: ( L is completely-distributive iff ( L is distributive & L is continuous & L opp is continuous ) ) thus ( L is completely-distributive implies ( L is distributive & L is continuous & L ~ is continuous ) ) by Lm3; ::_thesis: ( L is distributive & L is continuous & L opp is continuous implies L is completely-distributive ) assume that A1: ( L is distributive & L is continuous ) and A2: L ~ is continuous ; ::_thesis: L is completely-distributive reconsider L = L as distributive continuous LATTICE by A1; for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) by A2, Lm4; hence L is completely-distributive by Lm2; ::_thesis: verum end;