waybel_6.miz



    begin

    reserve x,y,Y,Z for set,

L for LATTICE,

l for Element of L;

    scheme :: WAYBEL_6:sch1

    NonUniqExD1 { Z() -> non empty RelStr , X() -> Subset of Z() , Y() -> non empty Subset of Z() , P[ object, object] } :

ex f be Function of X(), Y() st for e be Element of Z() st e in X() holds ex u be Element of Z() st u in Y() & u = (f . e) & P[e, u]

      provided

       A1: for e be Element of Z() st e in X() holds ex u be Element of Z() st u in Y() & P[e, u];

      

       A2: for e be object st e in X() holds ex u be object st u in Y() & P[e, u]

      proof

        let e be object;

        assume

         A3: e in X();

        then

        reconsider e1 = e as Element of X();

        reconsider e1 as Element of Z() by A3;

        consider u be Element of Z() such that

         A4: u in Y() & P[e1, u] by A1, A3;

        reconsider u1 = u as set;

        take u1;

        thus thesis by A4;

      end;

      consider f be Function such that

       A5: ( dom f) = X() & ( rng f) c= Y() and

       A6: for e be object st e in X() holds P[e, (f . e)] from FUNCT_1:sch 6( A2);

      reconsider f as Function of X(), Y() by A5, FUNCT_2:def 1, RELSET_1: 4;

      take f;

      for e be Element of Z() st e in X() holds ex u be Element of Z() st u in Y() & u = (f . e) & P[e, u]

      proof

        let e be Element of Z();

        assume

         A7: e in X();

        then

        reconsider e1 = (f . e) as Element of Y() by FUNCT_2: 5;

        reconsider fe = e1 as Element of Z();

        take fe;

        thus thesis by A6, A7;

      end;

      hence thesis;

    end;

    definition

      let L be non empty 1-sorted;

      let C,D be non empty Subset of L;

      let f be Function of C, D;

      let c be Element of C;

      :: original: .

      redefine

      func f . c -> Element of L ;

      coherence

      proof

        (f . c) in D;

        hence thesis;

      end;

    end

    registration

      let L be non empty Poset;

      cluster -> filtered directed for Chain of L;

      coherence

      proof

        let C be Chain of L;

        

         A1: the InternalRel of L is_strongly_connected_in C by ORDERS_2:def 7;

        thus C is filtered

        proof

          let x,y be Element of L;

          

           A2: x <= x & y <= y;

          assume

           A3: x in C & y in C;

          then [x, y] in the InternalRel of L or [y, x] in the InternalRel of L by A1;

          then x <= y or y <= x by ORDERS_2:def 5;

          hence thesis by A3, A2;

        end;

        let x,y be Element of L;

        

         A4: x <= x & y <= y;

        assume

         A5: x in C & y in C;

        then [x, y] in the InternalRel of L or [y, x] in the InternalRel of L by A1;

        then x <= y or y <= x by ORDERS_2:def 5;

        hence thesis by A5, A4;

      end;

    end

    registration

      cluster strict continuous distributive lower-bounded for LATTICE;

      existence

      proof

        set x1 = the set, R = the Order of {x1};

        take RelStr (# {x1}, R #);

        thus thesis;

      end;

    end

    theorem :: WAYBEL_6:1

    

     Th1: for S,T be Semilattice, f be Function of S, T holds f is meet-preserving iff for x,y be Element of S holds (f . (x "/\" y)) = ((f . x) "/\" (f . y))

    proof

      let S,T be Semilattice, f be Function of S, T;

      

       A1: ( dom f) = the carrier of S by FUNCT_2:def 1;

      thus f is meet-preserving implies for x,y be Element of S holds (f . (x "/\" y)) = ((f . x) "/\" (f . y))

      proof

        assume

         A2: f is meet-preserving;

        let z,y be Element of S;

        

         A3: f preserves_inf_of {z, y} by A2;

        

         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

        .= ((f . z) "/\" (f . y)) by YELLOW_0: 40;

      end;

      assume

       A5: for x,y be Element of S holds (f . (x "/\" y)) = ((f . x) "/\" (f . y));

      for z,y be Element of S holds f preserves_inf_of {z, y}

      proof

        let z,y be Element of S;

        

         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 thesis by A7;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_6:2

    

     Th2: for S,T be sup-Semilattice, f be Function of S, T holds f is join-preserving iff for x,y be Element of S holds (f . (x "\/" y)) = ((f . x) "\/" (f . y))

    proof

      let S,T be sup-Semilattice, f be Function of S, T;

      

       A1: ( dom f) = the carrier of S by FUNCT_2:def 1;

      thus f is join-preserving implies for x,y be Element of S holds (f . (x "\/" y)) = ((f . x) "\/" (f . y))

      proof

        assume

         A2: f is join-preserving;

        let z,y be Element of S;

        

         A3: f preserves_sup_of {z, y} by A2;

        

         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

        .= ((f . z) "\/" (f . y)) by YELLOW_0: 41;

      end;

      assume

       A5: for x,y be Element of S holds (f . (x "\/" y)) = ((f . x) "\/" (f . y));

      for z,y be Element of S holds f preserves_sup_of {z, y}

      proof

        let z,y be Element of S;

        

         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 thesis by A7;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_6:3

    

     Th3: for S,T be LATTICE, f be Function of S, T st T is distributive & f is meet-preserving join-preserving one-to-one holds S is distributive

    proof

      let S,T be LATTICE, f be Function of S, T;

      assume that

       A1: T is distributive and

       A2: f is meet-preserving join-preserving one-to-one;

      let x,y,z be Element of S;

      (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

      .= (((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;

    end;

    registration

      let S,T be complete LATTICE;

      cluster sups-preserving for Function of S, T;

      existence

      proof

        set t = ( Bottom T);

        set f = (S --> t);

        take f;

        let X be Subset of S;

        assume ex_sup_of (X,S);

        thus ex_sup_of ((f .: X),T) by YELLOW_0: 17;

        (f .: X) c= ( rng f) & ( rng f) c= {t} by FUNCOP_1: 13, RELAT_1: 111;

        then (f .: X) c= {t};

        then

         A1: (f .: X) = {t} or (f .: X) = {} by ZFMISC_1: 33;

        per cases ;

          suppose X = {} ;

          then (f .: X) = {} ;

          then ( sup (f .: X)) = t by YELLOW_0:def 11;

          hence thesis;

        end;

          suppose X <> {} ;

          then

          reconsider X1 = X as non empty Subset of S;

          set x = the Element of X1;

          (f . x) in (f .: X) by FUNCT_2: 35;

          

          hence ( sup (f .: X)) = t by A1, YELLOW_0: 39

          .= (f . ( sup X));

        end;

      end;

    end

    

     Lm1: for S,T be with_suprema non empty Poset holds for f be Function of S, T holds f is directed-sups-preserving implies f is monotone

    proof

      let S,T be with_suprema non empty Poset;

      let f be Function of S, T;

      assume

       A1: f is directed-sups-preserving;

      let x,y be Element of S such that

       A2: x <= y;

      

       A3: y = (y "\/" x) by A2, YELLOW_0: 24;

      for a,b be Element of S st a in {x, y} & b in {x, y} holds ex z be Element of S st z in {x, y} & a <= z & b <= z

      proof

        let a,b be Element of S such that

         A4: a in {x, y} & b in {x, y};

        take y;

        thus y in {x, y} by TARSKI:def 2;

        thus thesis by A2, A4, TARSKI:def 2;

      end;

      then {x, y} is directed non empty;

      then

       A5: f preserves_sup_of {x, y} by A1;

      

       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 be 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

      .= (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;

      assume afx = (f . x) & bfy = (f . y);

      hence afx <= bfy by A8, YELLOW_0: 22;

    end;

    theorem :: WAYBEL_6:4

    

     Th4: for S,T be complete LATTICE, f be sups-preserving Function of S, T st T is meet-continuous & f is meet-preserving one-to-one holds S is meet-continuous

    proof

      let S,T be complete LATTICE, f be sups-preserving Function of S, T;

      assume that

       A1: T is meet-continuous and

       A2: f is meet-preserving one-to-one;

      S is satisfying_MC

      proof

        let x be Element of S, D be non empty directed Subset of S;

        

         A3: ex_sup_of (D,S) & f preserves_sup_of D by WAYBEL_0: 75, WAYBEL_0:def 33;

        reconsider Y = {x} as directed non empty 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 be Element of T : y in (f .: D) } by YELLOW_4: 42;

        

         A7: ( {(f . x)} "/\" (f .: D)) c= (f .: ( {x} "/\" D))

        proof

          let p be object;

          assume p in ( {(f . x)} "/\" (f .: D));

          then

          consider y be Element of T such that

           A8: p = ((f . x) "/\" y) and

           A9: y in (f .: D) by A6;

          consider k be object 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 as Element of S by A10;

          (x "/\" k) in { (x "/\" a) where a be 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;

          then p = (f . (x "/\" k)) by A8, A12, YELLOW_3: 8;

          hence thesis by A5, A13, FUNCT_1:def 6;

        end;

        

         A14: ( {x} "/\" D) = { (x "/\" y) where y be Element of S : y in D } by YELLOW_4: 42;

        

         A15: (f .: ( {x} "/\" D)) c= ( {(f . x)} "/\" (f .: D))

        proof

          let p be object;

          assume p in (f .: ( {x} "/\" D));

          then

          consider m be object 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 as Element of S by A16;

          consider a be 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;

          then

           A21: p = ((f . x) "/\" fa) by A18, A19, YELLOW_3: 8;

          fa in (f .: D) by A5, A20, FUNCT_1:def 6;

          hence thesis by A6, A21;

        end;

        (f . (x "/\" ( sup D))) = ((f . x) "/\" (f . ( sup D))) by A2, Th1

        .= ((f . x) "/\" ( sup X)) by A3

        .= ( 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;

        hence (x "/\" ( sup D)) = ( sup ( {x} "/\" D)) by A2;

      end;

      hence thesis;

    end;

    begin

    definition

      let L be non empty reflexive RelStr, X be Subset of L;

      :: WAYBEL_6:def1

      attr X is Open means

      : Def1: for x be Element of L st x in X holds ex y be Element of L st y in X & y << x;

    end

    theorem :: WAYBEL_6:5

    for L be up-complete LATTICE, X be upper Subset of L holds X is Open iff for x be Element of L st x in X holds ( waybelow x) meets X

    proof

      let L be up-complete LATTICE, X be upper Subset of L;

      hereby

        assume

         A1: X is Open;

        thus for x be Element of L st x in X holds ( waybelow x) meets X

        proof

          let x be Element of L;

          assume x in X;

          then

          consider y be Element of L such that

           A2: y in X and

           A3: y << x by A1;

          y in { y1 where y1 be Element of L : y1 << x } by A3;

          then y in ( waybelow x) by WAYBEL_3:def 3;

          hence thesis by A2, XBOOLE_0: 3;

        end;

      end;

      assume

       A4: for x be Element of L st x in X holds ( waybelow x) meets X;

      now

        let x1 be Element of L;

        assume x1 in X;

        then ( waybelow x1) meets X by A4;

        then

        consider y be object such that

         A5: y in ( waybelow x1) and

         A6: y in X by XBOOLE_0: 3;

        ( waybelow x1) = { y1 where y1 be Element of L : y1 << x1 } by WAYBEL_3:def 3;

        then ex z be Element of L st z = y & z << x1 by A5;

        hence ex z be Element of L st z in X & z << x1 by A6;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_6:6

    for L be up-complete LATTICE, X be upper Subset of L holds X is Open iff X = ( union { ( wayabove x) where x be Element of L : x in X })

    proof

      let L be up-complete LATTICE, X be upper Subset of L;

      hereby

        assume

         A1: X is Open;

        

         A2: X c= ( union { ( wayabove x) where x be Element of L : x in X })

        proof

          let z be object;

          assume

           A3: z in X;

          then

          reconsider x1 = z as Element of X;

          reconsider x1 as Element of L by A3;

          consider y be Element of L such that

           A4: y in X and

           A5: y << x1 by A1, A3;

          x1 in { y1 where y1 be 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 be Element of L : x in X } by A4;

          hence thesis by A6, TARSKI:def 4;

        end;

        ( union { ( wayabove x) where x be Element of L : x in X }) c= X

        proof

          let z be object;

          assume z in ( union { ( wayabove x) where x be Element of L : x in X });

          then

          consider Y be set such that

           A7: z in Y and

           A8: Y in { ( wayabove x) where x be Element of L : x in X } by TARSKI:def 4;

          consider x be Element of L such that

           A9: Y = ( wayabove x) and

           A10: x in X by A8;

          z in { y where y be Element of L : y >> x } by A7, A9, WAYBEL_3:def 4;

          then

          consider z1 be Element of L such that

           A11: z1 = z and

           A12: z1 >> x;

          x <= z1 by A12, WAYBEL_3: 1;

          hence thesis by A10, A11, WAYBEL_0:def 20;

        end;

        hence X = ( union { ( wayabove x) where x be Element of L : x in X }) by A2;

      end;

      assume

       A13: X = ( union { ( wayabove x) where x be Element of L : x in X });

      now

        let x1 be Element of L;

        assume x1 in X;

        then

        consider Y be set such that

         A14: x1 in Y and

         A15: Y in { ( wayabove x) where x be Element of L : x in X } by A13, TARSKI:def 4;

        consider x be Element of L such that

         A16: Y = ( wayabove x) and

         A17: x in X by A15;

        x1 in { y where y be Element of L : y >> x } by A14, A16, WAYBEL_3:def 4;

        then ex z1 be Element of L st z1 = x1 & z1 >> x;

        hence ex x be Element of L st x in X & x << x1 by A17;

      end;

      hence thesis;

    end;

    registration

      let L be up-complete lower-bounded LATTICE;

      cluster Open for Filter of L;

      existence

      proof

        take ( [#] L);

        now

          let x be Element of L;

          assume x in ( [#] L);

          ( Bottom L) << x by WAYBEL_3: 4;

          hence ex y be Element of L st y in ( [#] L) & y << x;

        end;

        hence thesis;

      end;

    end

    theorem :: WAYBEL_6:7

    for L be lower-bounded continuous LATTICE, x be Element of L holds ( wayabove x) is Open

    proof

      let L be lower-bounded continuous LATTICE, x be Element of L;

      for l be Element of L st l in ( wayabove x) holds ex y be Element of L st y in ( wayabove x) & y << l

      proof

        let l be Element of L;

        assume l in ( wayabove x);

        then x << l by WAYBEL_3: 8;

        then

        consider y be Element of L such that

         A1: x << y & y << l by WAYBEL_4: 52;

        take y;

        thus thesis by A1, WAYBEL_3: 8;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_6:8

    

     Th8: for L be lower-bounded continuous LATTICE, x,y be Element of L st x << y holds ex F be Open Filter of L st y in F & F c= ( wayabove x)

    proof

      let L be lower-bounded continuous LATTICE, x,y be Element of L;

      defpred P[ Element of L, Element of L] means $2 << $1;

      assume

       A1: x << y;

      then

      reconsider W = ( wayabove x) as non empty Subset of L by WAYBEL_3: 8;

      

       A2: for z be Element of L st z in W holds ex z1 be Element of L st z1 in W & P[z, z1]

      proof

        let z be Element of L;

        assume z in W;

        then x << z by WAYBEL_3: 8;

        then

        consider x9 be 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 thesis by A4;

      end;

      consider f be Function of W, W such that

       A5: for z be Element of L st z in W holds ex z1 be Element of L st z1 in W & z1 = (f . z) & P[z, z1] from NonUniqExD1( A2);

      set V = { ( uparrow z) where z be Element of L : ex n be Element of NAT st z = (( iter (f,n)) . y) };

      now

        let u1 be object;

        assume u1 in V;

        then ex z be Element of L st u1 = ( uparrow z) & ex n be Element of NAT st z = (( iter (f,n)) . y);

        hence u1 in ( bool the carrier of L);

      end;

      then

      reconsider V as Subset-Family of L by TARSKI:def 3;

      

       A6: for X,Y be Subset of L st X in V & Y in V holds ex Z be 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;

        assume that

         A7: X in V and

         A8: Y in V;

        consider z2 be Element of L such that

         A9: Y = ( uparrow z2) and

         A10: ex n be Element of NAT st z2 = (( iter (f,n)) . y) by A8;

        consider n2 be Element of NAT such that

         A11: z2 = (( iter (f,n2)) . y) by A10;

        consider z1 be Element of L such that

         A12: X = ( uparrow z1) and

         A13: ex n be Element of NAT st z1 = (( iter (f,n)) . y) by A7;

        set z = (z1 "/\" z2);

        consider n1 be Element of NAT such that

         A14: z1 = (( iter (f,n1)) . y) by A13;

        

         A15: for n,k be Element of NAT holds (( iter (f,(n + k))) . y1) <= (( iter (f,n)) . y1)

        proof

          let n be Element of NAT ;

          defpred P[ Nat] means (( iter (f,(n + ( In ($1, NAT ))))) . y1) <= (( iter (f,n)) . y1);

          

           A16: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume

             A17: (( iter (f,(n + ( In (k, NAT ))))) . y1) <= (( iter (f,n)) . y1);

            set nk = (( iter (f,(n + ( In (k, NAT ))))) . y1);

            nk in W by FUNCT_2: 5;

            then

            consider znk be Element of L such that znk in W and

             A18: znk = (f . nk) and

             A19: znk << nk by A5;

            ( dom ( iter (f,(n + ( In (k, NAT )))))) = 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 <= nk by A19, WAYBEL_3: 1;

            hence thesis by A17, A20, ORDERS_2: 3;

          end;

          

           A21: P[ 0 ];

          let k be Element of NAT ;

          for k be Nat holds P[k] from NAT_1:sch 2( A21, A16);

          then P[k];

          hence thesis;

        end;

         A22:

        now

          per cases ;

            suppose n1 <= n2;

            then

            consider k be 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 z) in V by A8, A9, YELLOW_0: 25;

          end;

            suppose n2 <= n1;

            then

            consider k be 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 z) in V by A7, A12, YELLOW_0: 25;

          end;

        end;

        z <= z2 by YELLOW_0: 23;

        then

         A25: ( uparrow z2) c= ( uparrow z) by WAYBEL_0: 22;

        z <= z1 by YELLOW_0: 23;

        then ( uparrow z1) c= ( uparrow z) by WAYBEL_0: 22;

        hence thesis by A12, A9, A22, A25, XBOOLE_1: 8;

      end;

      

       A26: for X be Subset of L st X in V holds X is filtered

      proof

        let X be Subset of L;

        assume X in V;

        then ex z be Element of L st X = ( uparrow z) & ex n be Element of NAT st z = (( iter (f,n)) . y);

        hence thesis;

      end;

      y <= y;

      then

       A27: y in ( uparrow y) by WAYBEL_0: 18;

      set F = ( union { ( uparrow z) where z be Element of L : ex n be Element of NAT st z = (( iter (f,n)) . y) });

      now

        let u1 be object;

        assume u1 in F;

        then

        consider Y be set such that

         A28: u1 in Y and

         A29: Y in { ( uparrow z) where z be Element of L : ex n be Element of NAT st z = (( iter (f,n)) . y) } by TARSKI:def 4;

        consider z be Element of L such that

         A30: Y = ( uparrow z) and ex n be Element of NAT st z = (( iter (f,n)) . y) by A29;

        reconsider z1 = {z} as Subset of L;

        u1 in { a where a be Element of L : ex b be Element of L st a >= b & b in z1 } by A28, A30, WAYBEL_0: 15;

        then ex a be Element of L st a = u1 & ex b be Element of L st a >= b & b in z1;

        hence u1 in the carrier of L;

      end;

      then

      reconsider F as Subset of L by TARSKI:def 3;

      

       A31: y in ( wayabove x) by A1, WAYBEL_3: 8;

       A32:

      now

        let u1 be Element of L;

        assume u1 in F;

        then

        consider Y be set such that

         A33: u1 in Y and

         A34: Y in { ( uparrow z) where z be Element of L : ex n be Element of NAT st z = (( iter (f,n)) . y) } by TARSKI:def 4;

        consider z be Element of L such that

         A35: Y = ( uparrow z) and

         A36: ex n be Element of NAT st z = (( iter (f,n)) . y) by A34;

        consider n be 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 be 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 be Element of L : ex n be 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 be Element of L : ex b be Element of L st a >= b & b in z1 } by A33, A35, WAYBEL_0: 15;

        then

        consider a be Element of L such that

         A42: a = u1 and

         A43: ex b be Element of L st a >= b & b in z1;

        consider b be 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 be Element of L st g in F & g << u1 by A42, A44, A39, A41, WAYBEL_3: 2;

      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 be Element of L : ex n be Element of NAT st z = (( iter (f,n)) . y) };

      for X be Subset of L st X in V holds X is upper

      proof

        let X be Subset of L;

        assume X in V;

        then ex z be Element of L st X = ( uparrow z) & ex n be Element of NAT st z = (( iter (f,n)) . y);

        hence thesis;

      end;

      then

      reconsider F as Open Filter of L by A27, A47, A26, A6, A32, Def1, TARSKI:def 4, WAYBEL_0: 28, WAYBEL_0: 47;

      take F;

      now

        let u1 be object;

        assume

         A48: u1 in F;

        then

        consider Y be set such that

         A49: u1 in Y and

         A50: Y in { ( uparrow z) where z be Element of L : ex n be Element of NAT st z = (( iter (f,n)) . y) } by TARSKI:def 4;

        reconsider u = u1 as Element of L by A48;

        consider z be Element of L such that

         A51: Y = ( uparrow z) and

         A52: ex n be 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;

      end;

      hence thesis by A27, A47, TARSKI:def 4;

    end;

    theorem :: WAYBEL_6:9

    

     Th9: for L be complete LATTICE, X be Open upper Subset of L holds for x be Element of L st x in (X ` ) holds ex m be Element of L st x <= m & m is_maximal_in (X ` )

    proof

      let L be complete LATTICE, X be Open upper Subset of L;

      let x be Element of L;

      set A = { C where C be Chain of L : C c= (X ` ) & x in C };

      reconsider x1 = {x} as Chain of L by ORDERS_2: 8;

      

       A1: for Z be set st Z <> {} & Z c= A & Z is c=-linear holds ( union Z) in A

      proof

        let Z be set;

        assume that

         A2: Z <> {} and

         A3: Z c= A and

         A4: Z is c=-linear;

        now

          let Y;

          assume Y in Z;

          then Y in A by A3;

          then ex C be Chain of L st Y = C & C c= (X ` ) & x in C;

          hence Y c= the carrier of L;

        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 object;

          assume that

           A5: a in UZ and

           A6: b in UZ;

          consider az be set such that

           A7: a in az and

           A8: az in Z by A5, TARSKI:def 4;

          consider bz be 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;

          then

           A11: az c= bz or bz c= az;

          bz in A by A3, A10;

          then

           A12: ex C be Chain of L st bz = C & C c= (X ` ) & x in C;

          az in A by A3, A8;

          then

           A13: ex C be Chain of L st az = C & C c= (X ` ) & x in C;

          reconsider bz as Chain of L by A12;

          reconsider 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 thesis by A7, A9, A11;

        end;

        then

        reconsider UZ as Chain of L by ORDERS_2:def 7;

         A14:

        now

          let Y;

          assume Y in Z;

          then Y in A by A3;

          then ex C be Chain of L st Y = C & C c= (X ` ) & x in C;

          hence Y c= (X ` );

        end;

        set Y = the Element of Z;

        Y in Z by A2;

        then Y in A by A3;

        then ex C be Chain of L st Y = 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 thesis by A15;

      end;

      assume x in (X ` );

      then

       A16: x1 c= (X ` ) by ZFMISC_1: 31;

      x in x1 by ZFMISC_1: 31;

      then x1 in A by A16;

      then

      consider Y1 be set such that

       A17: Y1 in A and

       A18: for Z st Z in A & Z <> Y1 holds not Y1 c= Z by A1, ORDERS_1: 67;

      consider Y be Chain of L such that

       A19: Y = Y1 and

       A20: Y c= (X ` ) and

       A21: x in Y by A17;

      set m = ( sup Y);

      m is_>=_than Y by YELLOW_0: 32;

      then

       A22: x <= m by A21;

      

       A23: m is_>=_than Y by YELLOW_0: 32;

       A24:

      now

        given y be Element of L such that

         A25: y in (X ` ) and

         A26: y > m;

        

         A27: not y in Y by A26, ORDERS_2: 6, A23;

        set Y2 = (Y \/ {y});

        

         A28: m <= y by A26, ORDERS_2:def 6;

        the InternalRel of L is_strongly_connected_in Y2

        proof

          let a,b be object;

          assume

           A29: a in Y2 & b in Y2;

          per cases by A29, XBOOLE_0:def 3;

            suppose

             A30: a in Y & b in Y;

            the InternalRel of L is_strongly_connected_in Y by ORDERS_2:def 7;

            hence thesis by A30;

          end;

            suppose

             A31: a in Y & b in {y};

            then

            reconsider a1 = a as Element of L;

            reconsider b1 = b as Element of L by A31;

            b1 = y & a1 <= m by A23, A31, TARSKI:def 1;

            then a1 <= b1 by A28, ORDERS_2: 3;

            hence thesis by ORDERS_2:def 5;

          end;

            suppose

             A32: a in {y} & b in Y;

            then

            reconsider a1 = b as Element of L;

            reconsider b1 = a as Element of L by A32;

            b1 = y & a1 <= m by A23, A32, TARSKI:def 1;

            then a1 <= b1 by A28, ORDERS_2: 3;

            hence thesis by ORDERS_2:def 5;

          end;

            suppose

             A33: a in {y} & b in {y};

            then

            reconsider a1 = a as Element of L;

            

             A34: a1 <= a1;

            a = y & b = y by A33, TARSKI:def 1;

            hence thesis by A34, ORDERS_2:def 5;

          end;

        end;

        then

        reconsider Y2 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 A by A35;

        hence contradiction by A18, A19, A27, A36, XBOOLE_1: 7;

      end;

      now

        assume m in X;

        then

        consider y be Element of L such that

         A37: y in X and

         A38: y << m by Def1;

        consider d be 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;

      end;

      then m in (X ` ) by XBOOLE_0:def 5;

      then m is_maximal_in (X ` ) by A24, WAYBEL_4: 55;

      hence thesis by A22;

    end;

    begin

    definition

      let G be non empty RelStr, g be Element of G;

      :: WAYBEL_6:def2

      attr g is meet-irreducible means for x,y be Element of G st g = (x "/\" y) holds x = g or y = g;

    end

    notation

      let G be non empty RelStr, g be Element of G;

      synonym g is irreducible for g is meet-irreducible;

    end

    definition

      let G be non empty RelStr, g be Element of G;

      :: WAYBEL_6:def3

      attr g is join-irreducible means for x,y be Element of G st g = (x "\/" y) holds x = g or y = g;

    end

    definition

      let L be non empty RelStr;

      :: WAYBEL_6:def4

      func IRR L -> Subset of L means

      : Def4: for x be Element of L holds x in it iff x is irreducible;

      existence

      proof

        defpred P[ Element of L] means $1 is irreducible;

        consider X be Subset of L such that

         A1: for x be Element of L holds x in X iff P[x] from SUBSET_1:sch 3;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X,Y be Subset of L such that

         A2: for x be Element of L holds x in X iff x is irreducible and

         A3: for x be Element of L holds x in Y iff x is irreducible;

        for x be object st x in Y holds x in X by A2, A3;

        then

         A4: Y c= X;

        for x be object st x in X holds x in Y by A3, A2;

        then X c= Y;

        hence thesis by A4;

      end;

    end

    theorem :: WAYBEL_6:10

    

     Th10: for L be upper-bounded antisymmetric with_infima non empty RelStr holds ( Top L) is irreducible

    proof

      let L be upper-bounded with_infima antisymmetric non empty RelStr;

      let x,y be Element of L;

      assume (x "/\" 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 thesis by A1, ORDERS_2: 2;

    end;

    registration

      let L be upper-bounded antisymmetric with_infima non empty RelStr;

      cluster irreducible for Element of L;

      existence

      proof

        take ( Top L);

        thus thesis by Th10;

      end;

    end

    theorem :: WAYBEL_6:11

    for L be Semilattice, x be Element of L holds x is irreducible iff for A be finite non empty Subset of L st x = ( inf A) holds x in A

    proof

      let L be Semilattice, I be Element of L;

      thus I is irreducible implies for A be finite non empty Subset of L st I = ( inf A) holds I in A

      proof

        defpred P[ set] means $1 is non empty & I = ( "/\" ($1,L)) implies I in $1;

        assume

         A1: for x,y be Element of L st I = (x "/\" y) holds I = x or I = y;

        let A be finite non empty Subset of L;

         A2:

        now

          let x,B be set such that

           A3: x in A and

           A4: B c= A and

           A5: P[B];

          thus P[(B \/ {x})]

          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 (B \/ {x}) is non empty and

             A6: I = ( "/\" ((B \/ {x}),L));

            per cases ;

              suppose

               A7: B = {} ;

              then ( "/\" ((B \/ {a}),L)) = a by YELLOW_0: 39;

              hence thesis by A6, A7, TARSKI:def 1;

            end;

              suppose

               A8: B <> {} ;

              

               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

                per cases by A1, A6, A11, A9;

                  suppose ( inf C) = I;

                  hence thesis by A5, A8, XBOOLE_0:def 3;

                end;

                  suppose

                   A12: a = I;

                  a in {a} by TARSKI:def 1;

                  hence thesis by A12, XBOOLE_0:def 3;

                end;

              end;

            end;

          end;

        end;

        

         A13: P[ {} ];

        

         A14: A is finite;

         P[A] from FINSET_1:sch 2( A14, A13, A2);

        hence thesis;

      end;

      assume

       A15: for A be finite non empty Subset of L st I = ( inf A) holds I in A;

      let a,b be Element of L;

      assume I = (a "/\" b);

      then I = ( inf {a, b}) by YELLOW_0: 40;

      then I in {a, b} by A15;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: WAYBEL_6:12

    for L be LATTICE, l be Element of L st (( uparrow l) \ {l}) is Filter of L holds l is irreducible

    proof

      let L be LATTICE, l be Element of L;

      set F = (( uparrow l) \ {l});

      assume

       A1: (( uparrow l) \ {l}) is Filter of L;

      now

        let x,y be Element of L;

        assume that

         A2: l = (x "/\" y) and

         A3: x <> l and

         A4: y <> l;

        l <= y by A2, YELLOW_0: 23;

        then y in ( uparrow l) by WAYBEL_0: 18;

        then

         A5: y in F by A4, ZFMISC_1: 56;

        l <= x by A2, YELLOW_0: 23;

        then x in ( uparrow l) by WAYBEL_0: 18;

        then x in F by A3, ZFMISC_1: 56;

        then

        consider z be Element of L such that

         A6: z in F and

         A7: z <= x & z <= y by A1, A5, WAYBEL_0:def 2;

        l >= z by A2, A7, YELLOW_0: 23;

        then l in F by A1, A6, WAYBEL_0:def 20;

        hence contradiction by ZFMISC_1: 56;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_6:13

    

     Th13: for L be LATTICE, p be Element of L, F be Filter of L st p is_maximal_in (F ` ) holds p is irreducible

    proof

      let L be LATTICE, p be Element of L, F be Filter of L such that

       A1: p is_maximal_in (F ` );

      set X = (the carrier of L \ F);

      

       A2: p in X by A1, WAYBEL_4: 55;

      now

        let x,y be Element of L;

        assume that

         A3: p = (x "/\" y) and

         A4: x <> p and

         A5: y <> p;

        p <= y by A3, YELLOW_0: 23;

        then

         A6: p < y by A5, ORDERS_2:def 6;

        now

          assume x in F & y in F;

          then

          consider z be 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;

        end;

        then

         A9: x in X or y in X 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;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_6:14

    

     Th14: for L be lower-bounded continuous LATTICE, x,y be Element of L st not y <= x holds ex p be Element of L st p is irreducible & x <= p & not y <= p

    proof

      let L be lower-bounded continuous LATTICE, x,y be Element of L such that

       A1: not y <= x;

      for x be Element of L holds ( waybelow x) is non empty directed;

      then

      consider u be Element of L such that

       A2: u << y and

       A3: not u <= x by A1, WAYBEL_3: 24;

      consider F be 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;

       not x in F by A3, WAYBEL_0: 18, A5, A6;

      then x in (the carrier of L \ F) by XBOOLE_0:def 5;

      then

      consider m be Element of L such that

       A7: x <= m and

       A8: m is_maximal_in (F ` ) by Th9;

      take m;

      

       A9: m in (F ` ) by A8, WAYBEL_4: 55;

      now

        assume y <= m;

        then m in F by A4, WAYBEL_0:def 20;

        hence contradiction by A9, XBOOLE_0:def 5;

      end;

      hence thesis by A7, A8, Th13;

    end;

    begin

    definition

      let L be non empty RelStr, X be Subset of L;

      :: WAYBEL_6:def5

      attr X is order-generating means for x be Element of L holds ex_inf_of ((( uparrow x) /\ X),L) & x = ( inf (( uparrow x) /\ X));

    end

    theorem :: WAYBEL_6:15

    

     Th15: for L be up-complete lower-bounded LATTICE, X be Subset of L holds X is order-generating iff for l be Element of L holds ex Y be Subset of X st l = ( "/\" (Y,L))

    proof

      let L be up-complete lower-bounded LATTICE, X be Subset of L;

      thus X is order-generating implies for l be Element of L holds ex Y be Subset of X st l = ( "/\" (Y,L))

      proof

        assume

         A1: X is order-generating;

        let l be Element of L;

        for x be object 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;

        hence thesis;

      end;

      thus (for l be Element of L holds ex Y be Subset of X st l = ( "/\" (Y,L))) implies X is order-generating

      proof

        assume

         A2: for l be Element of L holds ex Y be Subset of X st l = ( "/\" (Y,L));

        let l be Element of L;

        consider Y be Subset of X such that

         A3: l = ( "/\" (Y,L)) by A2;

        set S = (( uparrow l) /\ X);

        thus ex_inf_of (S,L) by YELLOW_0: 17;

        

         A4: for b be Element of L st b is_<=_than S holds b <= l

        proof

          let b be Element of L;

          assume

           A5: b is_<=_than S;

          now

            let x be Element of L;

            assume

             A6: x in Y;

            l is_<=_than Y by A3, YELLOW_0: 33;

            then l <= x by A6;

            then x in ( uparrow l) by WAYBEL_0: 18;

            then x in S by A6, XBOOLE_0:def 4;

            hence b <= x by A5;

          end;

          then b is_<=_than Y;

          hence thesis by A3, YELLOW_0: 33;

        end;

        now

          let x be Element of L;

          assume x in S;

          then x in ( uparrow l) by XBOOLE_0:def 4;

          hence l <= x by WAYBEL_0: 18;

        end;

        then l is_<=_than S;

        hence thesis by A4, YELLOW_0: 33;

      end;

    end;

    theorem :: WAYBEL_6:16

    for L be up-complete lower-bounded LATTICE, X be Subset of L holds X is order-generating iff for Y be Subset of L st X c= Y & for Z be Subset of Y holds ( "/\" (Z,L)) in Y holds the carrier of L = Y

    proof

      let L be up-complete lower-bounded LATTICE, X be Subset of L;

      thus X is order-generating implies for Y be Subset of L st X c= Y & for Z be Subset of Y holds ( "/\" (Z,L)) in Y holds the carrier of L = Y

      proof

        assume

         A1: X is order-generating;

        let Y be Subset of L;

        assume that

         A2: X c= Y and

         A3: for Z be Subset of Y holds ( "/\" (Z,L)) in Y;

        now

          let l1 be object;

          assume l1 in the carrier of L;

          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;

          l = ( inf (( uparrow l) /\ X)) by A1;

          hence l1 in Y by A3, A4;

        end;

        hence the carrier of L c= Y;

        thus thesis;

      end;

      thus (for Y be Subset of L st X c= Y & for Z be Subset of Y holds ( "/\" (Z,L)) in Y holds the carrier of L = Y) implies X is order-generating

      proof

        set Y = { ( "/\" (Z,L)) where Z be Subset of L : Z c= X };

        now

          let x be object;

          assume x in Y;

          then ex Z be Subset of L st x = ( "/\" (Z,L)) & Z c= X;

          hence x in the carrier of L;

        end;

        then

        reconsider Y as Subset of L by TARSKI:def 3;

        now

          let x be object;

          assume

           A5: x in X;

          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;

        end;

        then

         A7: X c= Y;

        assume

         A8: for Y be Subset of L st X c= Y & for Z be Subset of Y holds ( "/\" (Z,L)) in Y holds the carrier of L = Y;

        for l be Element of L holds ex Z be Subset of X st l = ( "/\" (Z,L))

        proof

          let l be Element of L;

          for Z be Subset of Y holds ( "/\" (Z,L)) in Y

          proof

            let Z be Subset of Y;

            set S = ( union { A where A be Subset of L : A c= X & ( "/\" (A,L)) in Z });

            now

              let x be object;

              assume x in S;

              then

              consider Y be set such that

               A9: x in Y and

               A10: Y in { A where A be Subset of L : A c= X & ( "/\" (A,L)) in Z } by TARSKI:def 4;

              ex A be Subset of L st Y = A & A c= X & ( "/\" (A,L)) in Z by A10;

              hence x in the carrier of L by A9;

            end;

            then

            reconsider S as Subset of L by TARSKI:def 3;

            defpred P[ Subset of L] means $1 c= X & ( "/\" ($1,L)) in Z;

            set N = { ( "/\" (A,L)) where A be Subset of L : P[A] };

            now

              let x be object;

              assume

               A11: x in Z;

              then x in Y;

              then ex Z be Subset of L st x = ( "/\" (Z,L)) & Z c= X;

              hence x in N by A11;

            end;

            then

             A12: Z c= N;

            now

              let B be set;

              assume B in { A where A be Subset of L : A c= X & ( "/\" (A,L)) in Z };

              then ex A be Subset of L st B = A & A c= X & ( "/\" (A,L)) in Z;

              hence B c= X;

            end;

            then

             A13: S c= X by ZFMISC_1: 76;

            now

              let x be object;

              assume x in N;

              then ex S be Subset of L st x = ( "/\" (S,L)) & S c= X & ( "/\" (S,L)) in Z;

              hence x in Z;

            end;

            then N c= Z;

            

            then ( "/\" (Z,L)) = ( "/\" (N,L)) by A12, XBOOLE_0:def 10

            .= ( "/\" (( union { A where A be Subset of L : P[A] }),L)) from YELLOW_3:sch 3;

            hence thesis by A13;

          end;

          then the carrier of L = Y by A8, A7;

          then l in Y;

          then ex Z be Subset of L st l = ( "/\" (Z,L)) & Z c= X;

          hence thesis;

        end;

        hence thesis by Th15;

      end;

    end;

    theorem :: WAYBEL_6:17

    

     Th17: for L be up-complete lower-bounded LATTICE, X be Subset of L holds X is order-generating iff for l1,l2 be Element of L st not l2 <= l1 holds ex p be Element of L st p in X & l1 <= p & not l2 <= p

    proof

      let L be up-complete lower-bounded LATTICE, X be Subset of L;

      thus X is order-generating implies for l1,l2 be Element of L st not l2 <= l1 holds ex p be Element of L st p in X & l1 <= p & not l2 <= p

      proof

        assume

         A1: X is order-generating;

        let l1,l2 be Element of L;

        consider P be Subset of X such that

         A2: l1 = ( "/\" (P,L)) by A1, Th15;

        assume

         A3: not l2 <= l1;

        now

          assume for p be Element of L st p in P holds l2 <= p;

          then l2 is_<=_than P;

          hence contradiction by A3, A2, YELLOW_0: 33;

        end;

        then

        consider p be Element of L such that

         A4: p in P & not l2 <= p;

        take p;

        l1 is_<=_than P by A2, YELLOW_0: 33;

        hence thesis by A4;

      end;

      thus (for l1,l2 be Element of L st not l2 <= l1 holds ex p be Element of L st p in X & l1 <= p & not l2 <= p) implies X is order-generating

      proof

        assume

         A5: for l1,l2 be Element of L st not l2 <= l1 holds ex p be Element of L st p in X & l1 <= p & not l2 <= p;

        let l be Element of L;

        set y = ( inf (( uparrow l) /\ X));

        thus ex_inf_of ((( uparrow l) /\ X),L) by YELLOW_0: 17;

        

         A6: y is_<=_than (( uparrow l) /\ X) by YELLOW_0: 33;

        now

          l is_<=_than (( uparrow l) /\ X)

          proof

            let b be Element of L;

            assume b in (( uparrow l) /\ X);

            then b in ( uparrow l) by XBOOLE_0:def 4;

            hence thesis by WAYBEL_0: 18;

          end;

          then l <= y by YELLOW_0: 33;

          then

           A7: not y < l by ORDERS_2: 6;

          assume

           A8: y <> l;

          now

            per cases by A7, ORDERS_2:def 6;

              suppose not y <= l;

              then

              consider p be Element of L such that

               A9: p in X and

               A10: l <= p and

               A11: not y <= 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;

            end;

              suppose y = l;

              hence contradiction by A8;

            end;

          end;

          hence contradiction;

        end;

        hence thesis;

      end;

    end;

    theorem :: WAYBEL_6:18

    

     Th18: for L be lower-bounded continuous LATTICE, X be Subset of L st X = (( IRR L) \ {( Top L)}) holds X is order-generating

    proof

      let L be lower-bounded continuous LATTICE, X be Subset of L;

      assume

       A1: X = (( IRR L) \ {( Top L)});

      for l1,l2 be Element of L st not l2 <= l1 holds ex p be Element of L st p in X & l1 <= p & not l2 <= p

      proof

        let x,y be Element of L;

        assume not y <= x;

        then

        consider p be 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 thesis by A3, A4;

      end;

      hence thesis by Th17;

    end;

    theorem :: WAYBEL_6:19

    

     Th19: for L be lower-bounded continuous LATTICE, X,Y be Subset of L st X is order-generating & X c= Y holds Y is order-generating

    proof

      let L be lower-bounded continuous LATTICE, X,Y be Subset of L;

      assume that

       A1: X is order-generating and

       A2: X c= Y;

      let x be Element of L;

      thus ex_inf_of ((( uparrow x) /\ Y),L) by YELLOW_0: 17;

      

       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;

      hence thesis by A4, ORDERS_2: 2;

    end;

    begin

    definition

      let L be non empty RelStr;

      let l be Element of L;

      :: WAYBEL_6:def6

      attr l is prime means for x,y be Element of L st (x "/\" y) <= l holds x <= l or y <= l;

    end

    definition

      let L be non empty RelStr;

      :: WAYBEL_6:def7

      func PRIME L -> Subset of L means

      : Def7: for x be Element of L holds x in it iff x is prime;

      existence

      proof

        defpred P[ Element of L] means $1 is prime;

        consider X be Subset of L such that

         A1: for x be Element of L holds x in X iff P[x] from SUBSET_1:sch 3;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X,Y be Subset of L;

        assume that

         A2: for x be Element of L holds x in X iff x is prime and

         A3: for x be Element of L holds x in Y iff x is prime;

        thus X c= Y by A2, A3;

        thus Y c= X by A3, A2;

      end;

    end

    definition

      let L be non empty RelStr;

      let l be Element of L;

      :: WAYBEL_6:def8

      attr l is co-prime means (l ~ ) is prime;

    end

    theorem :: WAYBEL_6:20

    

     Th20: for L be upper-bounded antisymmetric non empty RelStr holds ( Top L) is prime by YELLOW_0: 45;

    theorem :: WAYBEL_6:21

    for L be lower-bounded antisymmetric non empty RelStr holds ( Bottom L) is co-prime

    proof

      let L be lower-bounded antisymmetric non empty RelStr;

      ( Top (L ~ )) is prime by Th20;

      hence (( Bottom L) ~ ) is prime by YELLOW_7: 33;

    end;

    registration

      let L be upper-bounded antisymmetric non empty RelStr;

      cluster prime for Element of L;

      existence

      proof

        take ( Top L);

        thus thesis by Th20;

      end;

    end

    theorem :: WAYBEL_6:22

    

     Th22: for L be Semilattice, l be Element of L holds l is prime iff for A be finite non empty Subset of L st l >= ( inf A) holds ex a be Element of L st a in A & l >= a

    proof

      let L be Semilattice, l be Element of L;

      thus l is prime implies for A be finite non empty Subset of L st l >= ( inf A) holds ex a be Element of L st a in A & l >= a

      proof

        defpred P[ set] means $1 is non empty & l >= ( "/\" ($1,L)) implies (ex k be Element of L st k in $1 & l >= k);

        assume

         A1: for x,y be Element of L st l >= (x "/\" y) holds l >= x or l >= y;

        let A be finite non empty Subset of L;

         A2:

        now

          let x,B be set such that

           A3: x in A and

           A4: B c= A and

           A5: P[B];

          thus P[(B \/ {x})]

          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 (B \/ {x}) is non empty and

             A6: l >= ( "/\" ((B \/ {x}),L));

            per cases ;

              suppose B = {} ;

              then ( "/\" ((B \/ {a}),L)) = a & a in (B \/ {a}) by TARSKI:def 1, YELLOW_0: 39;

              hence thesis by A6;

            end;

              suppose

               A7: B <> {} ;

              

               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

                per cases by A1, A6, A10, A8;

                  suppose ( inf C) <= l;

                  then

                  consider b be 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 thesis by A12;

                end;

                  suppose

                   A13: a <= l;

                  a in {a} by TARSKI:def 1;

                  then a in (B \/ {x}) by XBOOLE_0:def 3;

                  hence thesis by A13;

                end;

              end;

            end;

          end;

        end;

        

         A14: P[ {} ];

        

         A15: A is finite;

         P[A] from FINSET_1:sch 2( A15, A14, A2);

        hence thesis;

      end;

      assume

       A16: for A be finite non empty Subset of L st l >= ( inf A) holds ex a be Element of L st a in A & l >= a;

      let a,b be Element of L;

      set A = {a, b};

      

       A17: ( inf A) = (a "/\" b) by YELLOW_0: 40;

      assume (a "/\" b) <= l;

      then ex k be Element of L st k in A & l >= k by A16, A17;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: WAYBEL_6:23

    

     Th23: for L be sup-Semilattice, x be Element of L holds x is co-prime iff for A be finite non empty Subset of L st x <= ( sup A) holds ex a be Element of L st a in A & x <= a

    proof

      let L be sup-Semilattice, x be Element of L;

      thus x is co-prime implies for A be finite non empty Subset of L st x <= ( sup A) holds ex a be Element of L st a in A & x <= a

      proof

        assume x is co-prime;

        then

         A1: (x ~ ) is prime;

        let A be finite non empty Subset of L;

        reconsider A1 = A as finite non empty Subset of (L ~ );

        assume x <= ( sup 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

          let y be Element of (L ~ );

          assume y is_<=_than A;

          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;

        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 be Element of (L ~ ) such that

         A6: a in A1 & (x ~ ) >= a by A1, A2, Th22;

        take ( ~ a);

        thus thesis by A6, YELLOW_7: 2;

      end;

      thus (for A be finite non empty Subset of L st x <= ( sup A) holds ex a be Element of L st a in A & x <= a) implies x is co-prime

      proof

        assume

         A7: for A be finite non empty Subset of L st x <= ( sup A) holds ex a be Element of L st a in A & x <= a;

        now

          let a,b be Element of (L ~ );

          set A = {( ~ a), ( ~ b)};

          assume (a "/\" b) <= (x ~ );

          then x <= ( ~ (a "/\" b)) by YELLOW_7: 2;

          then ( sup A) = (( ~ a) "\/" ( ~ b)) & x <= (( ~ a) "\/" ( ~ b)) by YELLOW_0: 41, YELLOW_7: 24;

          then

          consider l be Element of L such that

           A8: l in A 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;

        end;

        then (x ~ ) is prime;

        hence thesis;

      end;

    end;

    theorem :: WAYBEL_6:24

    

     Th24: for L be LATTICE, l be Element of L st l is prime holds l is irreducible

    proof

      let L be LATTICE, l be Element of L;

      assume

       A1: l is prime;

      let x,y be Element of L;

      assume

       A2: l = (x "/\" y);

      then (x "/\" y) <= l;

      then

       A3: x <= l or y <= l by A1;

      l <= x & l <= y by A2, YELLOW_0: 23;

      hence thesis by A3, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_6:25

    

     Th25: for l holds l is prime iff for x be set, f be Function of L, ( BoolePoset {x}) st (for p be Element of L holds (f . p) = {} iff p <= l) holds f is meet-preserving join-preserving

    proof

      let l;

      thus l is prime implies for x be set, f be Function of L, ( BoolePoset {x}) st (for p be Element of L holds (f . p) = {} iff p <= l) holds f is meet-preserving join-preserving

      proof

        assume

         A1: l is prime;

        let x be set, f be Function of L, ( BoolePoset {x});

        assume

         A2: for p be Element of L holds (f . p) = {} iff p <= l;

        

         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 be Element of L holds f preserves_inf_of {z, y}

        proof

          let z,y be Element of L;

          

           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

            per cases by A3, TARSKI:def 2;

              suppose

               A8: (f . z) = {} & (f . 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;

            end;

              suppose

               A10: (f . z) = {x} & (f . y) = {x};

              then ( not y <= l) & not z <= l by A2;

              then not (z "/\" y) <= l by A1;

              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;

            end;

              suppose

               A12: (f . z) = {} & (f . y) = {x};

              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;

            end;

              suppose

               A14: (f . z) = {x} & (f . 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;

            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 thesis by A6;

        end;

        hence f is meet-preserving;

        for z,y be Element of L holds f preserves_sup_of {z, y}

        proof

          let z,y be Element of L;

          

           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

            per cases by A3, TARSKI:def 2;

              suppose

               A19: (f . z) = {} & (f . 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;

            end;

              suppose

               A21: (f . z) = {x} & (f . y) = {x};

              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;

            end;

              suppose

               A23: (f . z) = {} & (f . y) = {x};

              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;

            end;

              suppose

               A25: (f . z) = {x} & (f . 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;

            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 thesis by A17;

        end;

        hence thesis;

      end;

      thus (for x be set, f be Function of L, ( BoolePoset {x}) st (for p be Element of L holds (f . p) = {} iff p <= l) holds f is meet-preserving join-preserving) implies l is prime

      proof

        defpred P[ Element of L, set] means $1 <= l iff $2 = {} ;

        assume

         A27: for x be set, f be Function of L, ( BoolePoset {x}) st (for p be Element of L holds (f . p) = {} iff p <= l) holds f is meet-preserving join-preserving;

        let z,y be Element of 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 be Element of L holds ex b be Element of ( BoolePoset { {} }) st P[a, b]

        proof

          let a be Element of L;

          now

            per cases ;

              suppose

               A30: a <= l;

              set b = {} ;

              reconsider b as Element of ( BoolePoset { {} }) by A28, TARSKI:def 2;

              a <= l iff b = {} by A30;

              hence thesis;

            end;

              suppose

               A31: not a <= l;

              set b = { {} };

              reconsider b as Element of ( BoolePoset { {} }) by A28, TARSKI:def 2;

              a <= l iff b = {} by A31;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        consider f be Function of L, ( BoolePoset { {} }) such that

         A32: for p be Element of L holds P[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 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;

        

        then

         A35: {} = (f . (z "/\" y)) by A32

        .= (f . ( inf {z, y})) by YELLOW_0: 40

        .= ( inf {(f . z), (f . y)}) by A34, A33

        .= ((f . z) "/\" (f . y)) by YELLOW_0: 40

        .= ((f . z) /\ (f . y)) by YELLOW_1: 17;

        now

          assume ( not (f . z) = {} ) & not (f . y) = {} ;

          then (f . z) = { {} } & (f . y) = { {} } by A28, TARSKI:def 2;

          hence contradiction by A35;

        end;

        hence z <= l or y <= l by A32;

      end;

    end;

    theorem :: WAYBEL_6:26

    

     Th26: for L be upper-bounded LATTICE, l be 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, l be Element of L;

      set X1 = (the carrier of L \ ( downarrow l));

      reconsider X = X1 as Subset of L;

      assume

       A1: l <> ( Top L);

      thus l is prime implies (( downarrow l) ` ) is Filter of L

      proof

        assume

         A2: l is prime;

         A3:

        now

          let x,y be Element of L;

          assume that

           A4: x in X and

           A5: y in X;

           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;

           not (x "/\" y) in ( downarrow l) by A2, A7, A6, WAYBEL_0: 17;

          then

           A8: (x "/\" y) in X by XBOOLE_0:def 5;

          (x "/\" y) <= x & (x "/\" y) <= y by YELLOW_0: 23;

          hence ex z be Element of L st z in X & z <= x & z <= y by A8;

        end;

         A9:

        now

          let x,y be Element of L;

          assume that

           A10: x in X and

           A11: x <= y;

           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;

        end;

        now

          assume ( Top L) in ( downarrow l);

          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;

        end;

        hence thesis by A3, A9, WAYBEL_0:def 2, WAYBEL_0:def 20, XBOOLE_0:def 5;

      end;

      thus (( downarrow l) ` ) is Filter of L implies l is prime

      proof

        l <= l;

        then

         A12: l in ( downarrow l) by WAYBEL_0: 17;

        assume

         A13: (( downarrow l) ` ) is Filter of L;

        let x,y be Element of L;

        assume

         A14: (x "/\" y) <= l;

        now

          assume that

           A15: not x <= l and

           A16: not y <= l;

           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 be 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;

        end;

        hence x <= l or y <= l;

      end;

    end;

    theorem :: WAYBEL_6:27

    

     Th27: for L be distributive LATTICE holds for l be Element of L holds l is prime iff l is irreducible

    proof

      let L be distributive LATTICE, l be Element of L;

      thus l is prime implies l is irreducible by Th24;

      thus l is irreducible implies l is prime

      proof

        assume

         A1: l is irreducible;

        let x,y be Element of L;

        assume (x "/\" 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;

        hence x <= l or y <= l by YELLOW_0: 24;

      end;

    end;

    theorem :: WAYBEL_6:28

    

     Th28: for L be distributive LATTICE holds ( PRIME L) = ( IRR L)

    proof

      let L be distributive LATTICE;

      now

        let l1 be object;

        assume

         A1: l1 in ( PRIME L);

        then

        reconsider l = l1 as Element of ( PRIME L);

        reconsider 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;

      end;

      hence ( PRIME L) c= ( IRR L);

      now

        let l1 be object;

        assume

         A2: l1 in ( IRR L);

        then

        reconsider l = l1 as Element of ( IRR L);

        reconsider 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;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_6:29

    for L be Boolean LATTICE holds for l be Element of L st l <> ( Top L) holds l is prime iff for x be Element of L st x > l holds x = ( Top L)

    proof

      let L be Boolean LATTICE, l be Element of L;

      assume

       A1: l <> ( Top L);

      thus l is prime implies for x be Element of L st x > l holds x = ( Top L)

      proof

        assume

         A2: l is prime;

        let x be Element of L;

        consider y be Element of L such that

         A3: y is_a_complement_of x by WAYBEL_1:def 24;

        (x "/\" y) = ( Bottom L) by A3;

        then (x "/\" y) <= l by YELLOW_0: 44;

        then

         A4: x <= l or y <= l by A2;

        assume x > l;

        then y < x by A4, ORDERS_2: 7;

        then

         A5: y <= x by ORDERS_2:def 6;

        (x "\/" y) = ( Top L) by A3;

        hence thesis by A5, YELLOW_0: 24;

      end;

      thus (for x be Element of L st x > l holds x = ( Top L)) implies l is prime

      proof

        assume

         A6: for z be Element of L st z > l holds z = ( Top L);

        let x,y be Element of L;

        assume (x "/\" 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;

        

         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;

      end;

    end;

    theorem :: WAYBEL_6:30

    for L be continuous distributive lower-bounded LATTICE holds for l be Element of L st l <> ( Top L) holds l is prime iff ex F be Open Filter of L st l is_maximal_in (F ` )

    proof

      let L be continuous distributive lower-bounded LATTICE, l be Element of L;

      set F = (( downarrow l) ` );

      assume

       A1: l <> ( Top L);

      thus l is prime implies ex F be Open Filter of L st l is_maximal_in (F ` )

      proof

        

         A2: for x be Element of L holds ( waybelow x) is non empty directed;

         A3:

        now

          let x be Element of L;

          assume x in F;

          then not x in ( downarrow l) by XBOOLE_0:def 5;

          then not x <= l by WAYBEL_0: 17;

          then

          consider y be 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 F by XBOOLE_0:def 5;

          hence ex y be Element of L st y in F & y << x by A4;

        end;

        assume l is prime;

        then

        reconsider F as Open Filter of L by A1, A3, Def1, Th26;

        take F;

        

         A6: not ex y be Element of L st y in (F ` ) & y > l by WAYBEL_0: 17, ORDERS_2: 6;

        l <= l;

        then l in (F ` ) by WAYBEL_0: 17;

        hence thesis by A6, WAYBEL_4: 55;

      end;

      thus (ex F be Open Filter of L st l is_maximal_in (F ` )) implies l is prime

      proof

        assume ex O be Open Filter of L st l is_maximal_in (O ` );

        then

         A7: l is irreducible by Th13;

        now

          let x,y be Element of L;

          assume (x "/\" y) <= l;

          

          then l = (l "\/" (x "/\" y)) by YELLOW_0: 24

          .= ((l "\/" x) "/\" (l "\/" y)) by WAYBEL_1: 5;

          then

           A8: l = (l "\/" x) or l = (l "\/" y) by A7;

          assume ( not x <= l) & not y <= l;

          hence contradiction by A8, YELLOW_0: 24;

        end;

        hence thesis;

      end;

    end;

    theorem :: WAYBEL_6:31

    

     Th31: for L be RelStr, X be Subset of L holds ( chi (X,the carrier of L)) is Function of L, ( BoolePoset { {} })

    proof

      let L be RelStr, X be Subset of L;

      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 thesis;

    end;

    theorem :: WAYBEL_6:32

    

     Th32: for L be non empty RelStr, p,x be Element of L holds (( chi ((( downarrow p) ` ),the carrier of L)) . x) = {} iff x <= p

    proof

      let L be non empty RelStr, p,x be Element of L;

       not x in (( downarrow p) ` ) iff x in ( downarrow p) by XBOOLE_0:def 5;

      hence thesis by FUNCT_3:def 3, WAYBEL_0: 17;

    end;

    theorem :: WAYBEL_6:33

    

     Th33: for L be upper-bounded LATTICE, f be Function of L, ( BoolePoset { {} }), p be prime Element of L st ( chi ((( downarrow p) ` ),the carrier of L)) = f holds f is meet-preserving join-preserving

    proof

      let L be upper-bounded LATTICE, f be Function of L, ( BoolePoset { {} }), p be prime Element of L;

      assume ( chi ((( downarrow p) ` ),the carrier of L)) = f;

      then for x be Element of L holds (f . x) = {} iff x <= p by Th32;

      hence thesis by Th25;

    end;

    theorem :: WAYBEL_6:34

    

     Th34: for L be complete LATTICE st ( PRIME L) is order-generating holds L is distributive meet-continuous

    proof

      let L be complete LATTICE;

      set H = { ( chi ((( downarrow p) ` ),the carrier of L)) where p be Element of L : p is prime };

      set p9 = the prime Element of L;

      

       A1: ( chi ((( downarrow p9) ` ),the carrier of L)) in H;

      now

        let x be object;

        assume x in H;

        then ex p be Element of L st x = ( chi ((( downarrow p) ` ),the carrier of L)) & p is prime;

        hence x is Function;

      end;

      then

      reconsider H as functional non empty set by A1, FUNCT_1:def 13;

      deffunc F( object) = { f where f be Element of H : (f . $1) = 1 };

      consider F be Function such that

       A2: ( dom F) = the carrier of L and

       A3: for x be object st x in the carrier of L holds (F . x) = F(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 object;

        reconsider yy = y as set by TARSKI: 1;

        assume y in ( rng F);

        then

        consider x be object such that

         A5: x in ( dom F) & y = (F . x) by FUNCT_1:def 3;

        

         A6: y = { f where f be Element of H : (f . x) = 1 } by A2, A3, A5;

        yy c= H

        proof

          let p be object;

          assume p in yy;

          then ex f be Element of H st p = f & (f . x) = 1 by A6;

          hence thesis;

        end;

        hence thesis by A4;

      end;

      then

      reconsider 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;

        assume ex_inf_of ( {x, y},L);

        thus ex_inf_of ((F .: {x, y}),( BoolePoset H)) by YELLOW_0: 17;

        

         A8: { f where f be Element of H : (f . (x "/\" y)) = 1 } c= ({ f where f be Element of H : (f . x) = 1 } /\ { f where f be 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 object;

          

           A10: 1 = ( Top ( BoolePoset { {} })) by CARD_1: 49, YELLOW_1: 19;

          assume p in { f where f be Element of H : (f . (x "/\" y)) = 1 };

          then

          consider g be Element of H such that

           A11: g = p and

           A12: (g . (x "/\" y)) = 1;

          g in H;

          then

           A13: ex a be Element of L st ( chi ((( downarrow a) ` ),the carrier of L)) = g & a is prime;

          then

          reconsider g as Function of L, ( BoolePoset { {} }) by Th31;

          g is meet-preserving by A13, Th33;

          then

           A14: g preserves_inf_of {x, y};

          ( 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;

          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 be 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 be Element of H : (f . x) = 1 } by A11;

          hence thesis by A17, XBOOLE_0:def 4;

        end;

        

         A18: ({ f where f be Element of H : (f . x) = 1 } /\ { f where f be Element of H : (f . y) = 1 }) c= { f where f be Element of H : (f . (x "/\" y)) = 1 }

        proof

          let p be object;

          

           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 be Element of H : (f . x) = 1 } /\ { f where f be Element of H : (f . y) = 1 });

          then p in { f where f be Element of H : (f . x) = 1 } by XBOOLE_0:def 4;

          then

          consider f1 be Element of H such that

           A21: f1 = p and

           A22: (f1 . x) = 1;

          p in { f where f be Element of H : (f . y) = 1 } by A20, XBOOLE_0:def 4;

          then

           A23: ex f2 be Element of H st f2 = p & (f2 . y) = 1;

          f1 in H;

          then

          consider a be Element of L such that

           A24: ( chi ((( downarrow a) ` ),the carrier of L)) = f1 and

           A25: a is prime;

          reconsider f1 as Function of L, ( BoolePoset { {} }) by A24, Th31;

          for x be 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};

          ( 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

          .= 1 by A21, A22, A23, YELLOW_5: 2;

          hence thesis by A21;

        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 be Element of H : (f . x) = 1 } /\ (F . y)) by A3

        .= ({ f where f be Element of H : (f . x) = 1 } /\ { f where f be Element of H : (f . y) = 1 }) by A3

        .= { f where f be Element of H : (f . (x "/\" y)) = 1 } by A18, A8

        .= (F . (x "/\" y)) by A3

        .= (F . ( inf {x, y})) by YELLOW_0: 40;

      end;

      assume

       A28: ( PRIME L) is order-generating;

      

       A29: F is one-to-one

      proof

        let x1,x2 be object;

        assume that

         A30: x1 in ( dom F) and

         A31: x2 in ( dom F) and

         A32: (F . x1) = (F . x2);

        reconsider l2 = x2 as Element of L by A31;

        reconsider l1 = x1 as Element of L by A30;

        now

          

           A33: (F . l2) = { f where f be Element of H : (f . l2) = 1 } by A3;

          

           A34: (F . l1) = { f where f be Element of H : (f . l1) = 1 } by A3;

          assume

           A35: l1 <> l2;

          per cases by A35, ORDERS_2: 2;

            suppose not l1 <= l2;

            then

            consider p be 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 CH in H;

            then

            reconsider CH as Element of H;

             A39:

            now

              assume CH in (F . l2);

              then ex f be Element of H st f = CH & (f . l2) = 1 by A33;

              hence contradiction by A37, Th32;

            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;

          end;

            suppose not l2 <= l1;

            then

            consider p be 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 CH in H;

            then

            reconsider CH as Element of H;

             A43:

            now

              assume CH in (F . l1);

              then ex f be Element of H st f = CH & (f . l1) = 1 by A34;

              hence contradiction by A41, Th32;

            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;

          end;

        end;

        hence thesis;

      end;

      F is join-preserving

      proof

        let x,y be Element of L;

        assume ex_sup_of ( {x, y},L);

        thus ex_sup_of ((F .: {x, y}),( BoolePoset H)) by YELLOW_0: 17;

        

         A44: { f where f be Element of H : (f . (x "\/" y)) = 1 } c= ({ f where f be Element of H : (f . x) = 1 } \/ { f where f be Element of H : (f . y) = 1 })

        proof

          let p be object;

          

           A45: 1 = ( Top ( BoolePoset { {} })) by CARD_1: 49, YELLOW_1: 19;

          assume p in { f where f be Element of H : (f . (x "\/" y)) = 1 };

          then

          consider g be Element of H such that

           A46: g = p and

           A47: (g . (x "\/" y)) = 1;

          g in H;

          then

           A48: ex a be Element of L st ( chi ((( downarrow a) ` ),the carrier of L)) = g & a is prime;

          then

          reconsider g as Function of L, ( BoolePoset { {} }) by Th31;

          g is join-preserving by A48, Th33;

          then

           A49: g preserves_sup_of {x, y};

          ( 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

            assume (g . x) = {} & (g . y) = {} ;

            

            then ((g . x) "\/" (g . y)) = ( {} \/ {} ) by YELLOW_1: 17

            .= 0 ;

            hence contradiction by A47, A50, A49, A51, A52;

          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 be Element of H : (f . x) = 1 } or p in { f where f be Element of H : (f . y) = 1 } by A46, A45;

          hence thesis by XBOOLE_0:def 3;

        end;

        

         A56: ({ f where f be Element of H : (f . x) = 1 } \/ { f where f be Element of H : (f . y) = 1 }) c= { f where f be Element of H : (f . (x "\/" y)) = 1 }

        proof

          let p be object;

          assume

           A57: p in ({ f where f be Element of H : (f . x) = 1 } \/ { f where f be Element of H : (f . y) = 1 });

          per cases by A57, XBOOLE_0:def 3;

            suppose p in { f where f be Element of H : (f . x) = 1 };

            then

            consider f1 be Element of H such that

             A58: f1 = p and

             A59: (f1 . x) = 1;

            f1 in H;

            then

            consider a be Element of L such that

             A60: ( chi ((( downarrow a) ` ),the carrier of L)) = f1 and

             A61: a is prime;

            reconsider f1 as Function of L, ( BoolePoset { {} }) by A60, Th31;

            for x be 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};

            ( 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

            .= 1 by A59, A64, YELLOW_0: 24;

            hence thesis by A58;

          end;

            suppose p in { f where f be Element of H : (f . y) = 1 };

            then

            consider f1 be Element of H such that

             A66: f1 = p and

             A67: (f1 . y) = 1;

            f1 in H;

            then

            consider b be Element of L such that

             A68: ( chi ((( downarrow b) ` ),the carrier of L)) = f1 and

             A69: b is prime;

            reconsider f1 as Function of L, ( BoolePoset { {} }) by A68, Th31;

            for x be 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};

            ( 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

            .= 1 by A67, A72, YELLOW_0: 24;

            hence thesis by A66;

          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 be Element of H : (f . x) = 1 } \/ (F . y)) by A3

        .= ({ f where f be Element of H : (f . x) = 1 } \/ { f where f be Element of H : (f . y) = 1 }) by A3

        .= { f where f be Element of H : (f . (x "\/" y)) = 1 } by A56, A44

        .= (F . (x "\/" y)) by A3

        .= (F . ( sup {x, y})) by YELLOW_0: 41;

      end;

      hence L is distributive by A7, A29, Th3;

      F is sups-preserving

      proof

        let X be Subset of L;

        F preserves_sup_of X

        proof

          assume ex_sup_of (X,L);

          thus ex_sup_of ((F .: X),( BoolePoset H)) by YELLOW_0: 17;

          

           A74: (F . ( sup X)) = { g where g be Element of H : (g . ( sup X)) = 1 } by A3;

          

           A75: ( sup (F .: X)) c= (F . ( sup X))

          proof

            let a be object;

            assume a in ( sup (F .: X));

            then a in ( union (F .: X)) by YELLOW_1: 21;

            then

            consider Y be set such that

             A76: a in Y and

             A77: Y in (F .: X) by TARSKI:def 4;

            consider z be object 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 as Element of L by A78;

            (F . z) = { f where f be Element of H : (f . z) = 1 } by A3;

            then

            consider f be Element of H such that

             A81: a = f and

             A82: (f . z) = 1 by A76, A80;

            f in H;

            then

            consider p be Element of L such that

             A83: f = ( chi ((( downarrow p) ` ),the carrier of L)) and p is prime;

             A84:

            now

              ( sup X) is_>=_than X by YELLOW_0: 32;

              then

               A85: z <= ( sup X) by A79;

              assume (f . ( sup X)) = 0 ;

              then ( sup X) <= p by A83, Th32;

              then z <= p by A85, ORDERS_2: 3;

              hence contradiction by A82, A83, Th32;

            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 thesis by A74, A81, A84;

          end;

          (F . ( sup X)) c= ( sup (F .: X))

          proof

            let a be object;

            assume a in (F . ( sup X));

            then

            consider f be Element of H such that

             A87: a = f and

             A88: (f . ( sup X)) = 1 by A74;

            f in H;

            then

            consider p be 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

              assume for l be Element of L st l in X holds l <= p;

              then X is_<=_than p;

              hence contradiction by A91, YELLOW_0: 32;

            end;

            then

            consider l be 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 be 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 thesis by YELLOW_1: 21;

          end;

          hence thesis by A75;

        end;

        hence thesis;

      end;

      hence thesis by A7, A29, Th4;

    end;

    theorem :: WAYBEL_6:35

    

     Th35: for L be lower-bounded continuous LATTICE holds L is distributive iff ( PRIME L) is order-generating

    proof

      let L be lower-bounded continuous LATTICE;

      thus L is distributive implies ( PRIME L) is order-generating

      proof

        assume L is distributive;

        then

         A1: ( PRIME L) = ( IRR L) by Th28;

        (( IRR L) \ {( Top L)}) c= ( IRR L) by XBOOLE_1: 36;

        hence thesis by A1, Th18, Th19;

      end;

      thus thesis by Th34;

    end;

    theorem :: WAYBEL_6:36

    for L be lower-bounded continuous LATTICE holds L is distributive iff L is Heyting

    proof

      let L be lower-bounded continuous LATTICE;

      thus L is distributive implies L is Heyting

      proof

        assume L is distributive;

        then ( PRIME L) is order-generating by Th35;

        then L is distributive meet-continuous by Th34;

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: WAYBEL_6:37

    

     Th37: for L be continuous complete LATTICE st for l be Element of L holds ex X be Subset of L st l = ( sup X) & for x be Element of L st x in X holds x is co-prime holds for l be Element of L holds l = ( "\/" ((( waybelow l) /\ ( PRIME (L opp ))),L))

    proof

      let L be continuous complete LATTICE;

      defpred P[ object, object] means ex A be set st A = $2 & A c= ( PRIME (L ~ )) & $1 = ( "\/" (A,L));

      assume

       A1: for l be Element of L holds ex X be Subset of L st l = ( sup X) & for x be Element of L st x in X holds x is co-prime;

      

       A2: for e be object st e in the carrier of L holds ex u be object st P[e, u]

      proof

        let e be object;

        assume e in the carrier of L;

        then

        reconsider l = e as Element of L;

        consider X be Subset of L such that

         A3: l = ( sup X) and

         A4: for x be Element of L st x in X holds x is co-prime by A1;

        now

          let p1 be object;

          assume

           A5: p1 in X;

          then

          reconsider p = p1 as Element of L;

          p is co-prime by A4, A5;

          then (p ~ ) is prime;

          hence p1 in ( PRIME (L ~ )) by Def7;

        end;

        then X c= ( PRIME (L ~ ));

        hence thesis by A3;

      end;

      consider f be Function such that

       A6: ( dom f) = the carrier of L and

       A7: for e be object st e in the carrier of L holds P[e, (f . e)] from CLASSES1:sch 1( A2);

      let l be Element of L;

      

       A8: ex_sup_of ((( waybelow l) /\ ( PRIME (L ~ ))),L) by YELLOW_0: 17;

      

       A9: ( waybelow l) c= { ( sup X) where X be Subset of L : X in ( rng f) & ( sup X) in ( waybelow l) }

      proof

        let e be object;

        assume

         A10: e in ( waybelow l);

        then

         A11: P[e, (f . e)] by A7;

        then (f . e) c= ( PRIME (L ~ ));

        then

         A12: (f . e) c= the carrier of (L ~ ) by XBOOLE_1: 1;

        e = ( "\/" ((f . e),L)) & (f . e) in ( rng f) by A6, FUNCT_1:def 3, A11;

        hence thesis by A10, A12;

      end;

      defpred P[ Subset of L] means $1 in ( rng f) & ( sup $1) in ( waybelow l);

      

       A13: l = ( sup ( waybelow l)) by WAYBEL_3:def 5;

      set Z = ( union { X where X be Subset of L : X in ( rng f) & ( sup X) in ( waybelow l) });

      

       A14: Z c= (( waybelow l) /\ ( PRIME (L ~ )))

      proof

        let e be object;

        assume e in Z;

        then

        consider Y be set such that

         A15: e in Y and

         A16: Y in { X where X be Subset of L : X in ( rng f) & ( sup X) in ( waybelow l) } by TARSKI:def 4;

        consider X be Subset of L such that

         A17: Y = X and

         A18: X in ( rng f) and

         A19: ( sup X) in ( waybelow l) by A16;

        reconsider e1 = e as Element of L by A15, A17;

        e1 <= ( sup X) by A15, A17, YELLOW_2: 22;

        then

         A20: e in ( waybelow l) by A19, WAYBEL_0:def 19;

        consider r be object such that

         A21: r in ( dom f) & X = (f . r) by A18, FUNCT_1:def 3;

         P[r, (f . r)] by A6, A7, A21;

        then X c= ( PRIME (L ~ )) by A21;

        hence thesis by A15, A17, A20, XBOOLE_0:def 4;

      end;

      

       A22: ex_sup_of (Z,L) by YELLOW_0: 17;

       ex_sup_of (( waybelow l),L) by YELLOW_0: 17;

      then

       A23: ( "\/" ((( waybelow l) /\ ( PRIME (L ~ ))),L)) <= ( "\/" (( waybelow l),L)) by A8, XBOOLE_1: 17, YELLOW_0: 34;

      { ( sup X) where X be Subset of L : P[X] } c= ( waybelow l)

      proof

        let e be object;

        assume e in { ( sup X) where X be Subset of L : X in ( rng f) & ( sup X) in ( waybelow l) };

        then ex X be Subset of L st e = ( sup X) & X in ( rng f) & ( sup X) in ( waybelow l);

        hence thesis;

      end;

      

      then l = ( "\/" ({ ( sup X) where X be Subset of L : P[X] },L)) by A13, A9, XBOOLE_0:def 10

      .= ( "\/" (( union { X where X be Subset of L : P[X] }),L)) from YELLOW_3:sch 5;

      then l <= ( "\/" ((( waybelow l) /\ ( PRIME (L ~ ))),L)) by A22, A8, A14, YELLOW_0: 34;

      hence thesis by A13, A23, ORDERS_2: 2;

    end;

    

     Lm2: for L be continuous complete LATTICE st for l be Element of L holds ex X be Subset of L st l = ( sup X) & for x be Element of L st x in X holds x is co-prime holds L is completely-distributive

    proof

      let L be continuous complete LATTICE such that

       A1: for l be Element of L holds ex X be Subset of L st l = ( sup X) & for x be Element of L st x in X holds x is co-prime;

      thus L is complete;

      let J be non empty set, K be non-empty ManySortedSet of J;

      let F be DoubleIndexedSet of K, L;

      set l = ( Inf ( Sups F));

      set X = (( waybelow l) /\ ( PRIME (L ~ )));

      

       A2: X c= ( waybelow l) by XBOOLE_1: 17;

      reconsider X as Subset of L;

      

       A3: ( dom F) = J by PARTFUN1:def 2;

      

       A4: for x be Element of L st x in X holds x is co-prime

      proof

        let x be Element of L;

        assume x in X;

        then x in ( PRIME (L ~ )) by XBOOLE_0:def 4;

        then (x ~ ) is prime by Def7;

        hence thesis;

      end;

      

       A5: ( inf ( rng ( Sups F))) = ( Inf ( Sups F)) by YELLOW_2:def 6;

      X is_<=_than ( Sup ( Infs ( Frege F)))

      proof

        let p be Element of L;

        defpred P[ object, object] means $2 in (K . $1) & [p, ((F . $1) . $2)] in the InternalRel of L;

        assume

         A6: p in X;

        

         A7: for j be object st j in J holds ex k be object st P[j, k]

        proof

          let j1 be object;

          assume j1 in J;

          then

          reconsider j = j1 as Element of J;

          set k = the Element of (K . j);

          ( dom ( Sups F)) = J by A3, FUNCT_2:def 1;

          then

           A8: (( Sups F) . j) in ( rng ( Sups F)) by FUNCT_1:def 3;

          

           A9: p << l & ( Sup (F . j)) = ( sup ( rng (F . j))) by A2, A6, WAYBEL_3: 7, YELLOW_2:def 5;

          ( Sup (F . j)) = (( Sups F) . j) by A3, WAYBEL_5:def 1;

          then l <= ( Sup (F . j)) by A5, A8, YELLOW_2: 22;

          then

          consider A be 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) . k)}),L) by YELLOW_0: 17;

          then ( sup A) <= ( sup (A \/ {((F . j) . k)})) by XBOOLE_1: 7, YELLOW_0: 34;

          then

           A12: p <= ( sup (A \/ {((F . j) . k)})) by A11, ORDERS_2: 3;

          p is co-prime by A4, A6;

          then

          consider a be Element of L such that

           A13: a in (A \/ {((F . j) . k)}) and

           A14: p <= a by A12, Th23;

          per cases by A13, XBOOLE_0:def 3;

            suppose a in A;

            then

            consider k1 be object such that

             A15: k1 in ( dom (F . j)) and

             A16: a = ((F . j) . k1) by A10, FUNCT_1:def 3;

            reconsider 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 thesis;

          end;

            suppose a in {((F . j) . k)};

            then a = ((F . j) . k) by TARSKI:def 1;

            then [p, ((F . j) . k)] in the InternalRel of L by A14, ORDERS_2:def 5;

            hence thesis;

          end;

        end;

        consider f1 be Function such that

         A17: ( dom f1) = J and

         A18: for j be object st j in J holds P[j, (f1 . j)] from CLASSES1:sch 1( A7);

        now

          let g be object;

          assume g in ( dom ( doms F));

          then g in ( dom F) by FUNCT_6:def 2;

          hence g in ( dom f1) by A17;

        end;

        then

         A19: ( dom ( doms F)) c= ( dom f1);

        for g be object st g in ( dom f1) holds g in ( dom ( doms F)) by FUNCT_6:def 2, A3, A17;

        then ( dom f1) c= ( dom ( doms F));

        then

         A20: ( dom f1) = ( dom ( doms F)) by A19;

        

         A21: for b be object st b in ( dom ( doms F)) holds (f1 . b) in (( doms F) . b)

        proof

          let b be object;

          assume

           A22: b in ( dom ( doms F));

          then

           A23: (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, A22, FUNCT_6: 22

          .= (K . b) by A23, FUNCT_2:def 1;

          hence thesis by A17, A18, A19, A22;

        end;

        then

        reconsider D = ( product ( doms F)) as non empty set by A20, CARD_3: 9;

        reconsider f = f1 as Element of ( product ( doms F)) by A20, A21, CARD_3: 9;

        

         A24: f1 in ( product ( doms F)) by A20, A21, CARD_3: 9;

        p is_<=_than ( rng (( Frege F) . f))

        proof

          let b be Element of L;

          assume b in ( rng (( Frege F) . f));

          then

          consider a be object such that

           A25: a in ( dom (( Frege F) . f)) and

           A26: b = ((( Frege F) . f) . a) by FUNCT_1:def 3;

          reconsider a as Element of J by A25;

          f in ( dom ( Frege F)) by A24, 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 A26, ORDERS_2:def 5;

        end;

        then p <= ( inf ( rng (( Frege F) . f))) by YELLOW_0: 33;

        then

         A27: p <= ( Inf (( Frege F) . f)) 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 (R . f2)) in ( rng ( Infs R)) by WAYBEL_5: 14;

        then ( Inf (( Frege F) . f)) <= ( sup ( rng ( Infs ( Frege F)))) by YELLOW_2: 22;

        then ( Inf (( Frege F) . f)) <= ( Sup ( Infs ( Frege F))) by YELLOW_2:def 5;

        hence thesis by A27, ORDERS_2: 3;

      end;

      then

       A28: ( sup X) <= ( Sup ( Infs ( Frege F))) by YELLOW_0: 32;

      ( Inf ( Sups F)) >= ( Sup ( Infs ( Frege F))) & ( Inf ( Sups F)) = ( sup X) by A1, Th37, WAYBEL_5: 16;

      hence thesis by A28, ORDERS_2: 2;

    end;

    

     Lm3: for L be completely-distributive complete LATTICE holds L is distributive continuous & (L ~ ) is continuous

    proof

      let L be completely-distributive complete LATTICE;

      (L ~ ) is completely-distributive by YELLOW_7: 51;

      hence thesis;

    end;

    

     Lm4: for L be complete LATTICE st L is distributive continuous & (L ~ ) is continuous holds for l be Element of L holds ex X be Subset of L st l = ( sup X) & for x be Element of L st x in X holds x is co-prime

    proof

      let L be complete LATTICE;

      assume that

       A1: L is distributive continuous and

       A2: (L ~ ) is continuous;

      let l be Element of L;

      reconsider L as distributive continuous complete LATTICE by A1;

      reconsider l1 = l as Element of (L ~ );

      ( PRIME (L ~ )) is order-generating by A2, Th35;

      then

      consider Y be Subset of ( PRIME (L ~ )) such that

       A3: l1 = ( "/\" (Y,(L ~ ))) by Th15;

      reconsider Y as Subset of L by XBOOLE_1: 1;

      

       A4: for x be Element of L st x in Y holds x is co-prime by Def7;

       ex_sup_of (Y,L) by YELLOW_0: 17;

      then ( "\/" (Y,L)) = ( "/\" (Y,(L ~ ))) by YELLOW_7: 12;

      hence thesis by A3, A4;

    end;

    theorem :: WAYBEL_6:38

    for L be complete LATTICE holds L is completely-distributive iff L is continuous & for l be Element of L holds ex X be Subset of L st l = ( sup X) & for x be Element of L st x in X holds x is co-prime

    proof

      let L be complete LATTICE;

      thus L is completely-distributive implies L is continuous & for l be Element of L holds ex X be Subset of L st l = ( sup X) & for x be Element of L st x in X holds x is co-prime

      proof

        assume L is completely-distributive;

        then

        reconsider L as completely-distributive LATTICE;

        (L ~ ) is continuous by Lm3;

        hence thesis by Lm4;

      end;

      thus thesis by Lm2;

    end;

    theorem :: WAYBEL_6:39

    for L be complete LATTICE holds L is completely-distributive iff L is distributive continuous & (L opp ) is continuous

    proof

      let L be complete LATTICE;

      thus L is completely-distributive implies L is distributive continuous & (L ~ ) is continuous by Lm3;

      assume that

       A1: L is distributive continuous and

       A2: (L ~ ) is continuous;

      reconsider L as distributive continuous LATTICE by A1;

      for l be Element of L holds ex X be Subset of L st l = ( sup X) & for x be Element of L st x in X holds x is co-prime by A2, Lm4;

      hence thesis by Lm2;

    end;