lattice6.miz



    begin

    registration

      cluster finite for Lattice;

      existence

      proof

        set L = ( BooleLatt {} );

        the carrier of L = ( bool {} ) by LATTICE3:def 1;

        then L is finite;

        hence thesis;

      end;

    end

    

     Lm1: for L be finite Lattice holds for X be Subset of L holds X is empty or ex a be Element of ( LattPOSet L) st a in X & for b be Element of ( LattPOSet L) st b in X & b <> a holds not b <= a

    proof

      defpred P[ Nat] means for L be finite Lattice holds for X be Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X & ( len p) = $1 holds X is empty or ex a be Element of ( LattPOSet L) st a in X & for b be Element of ( LattPOSet L) st b in X & b <> a holds not (b <= a);

      let L be finite Lattice;

      let X be Subset of L;

      

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

      proof

        let k be Nat;

        assume

         A2: P[k];

        per cases ;

          suppose

           A3: k = 0 ;

          for L be finite Lattice holds for X be Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X & ( len p) = 1 holds ex a be Element of ( LattPOSet L) st a in X & for b be Element of ( LattPOSet L) st b in X & b <> a holds not b <= a

          proof

            let L be finite Lattice;

            let X be Subset of ( LattPOSet L);

            let p be FinSequence;

            assume that

             A4: ( rng p) = X and

             A5: ( len p) = 1;

            consider a be set such that

             A6: (p . 1) = a;

            

             A7: ( Seg 1) = ( dom p) by A5, FINSEQ_1:def 3;

            then 1 in ( dom p) by FINSEQ_1: 2, TARSKI:def 1;

            then

             A8: a in ( rng p) by A6, FUNCT_1:def 3;

            then

            reconsider a as Element of ( LattPOSet L) by A4;

            ( rng p) = {a} by A7, A6, FINSEQ_1: 2, FUNCT_1: 4;

            then for b be Element of ( LattPOSet L) st b in X & b <> a holds not b <= a by A4, TARSKI:def 1;

            hence thesis by A4, A8;

          end;

          hence thesis by A3;

        end;

          suppose

           A9: k <> 0 ;

          for L be finite Lattice holds for X be Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X & ( len p) = (k + 1) holds ex a be Element of ( LattPOSet L) st a in X & for b be Element of ( LattPOSet L) st b in X & b <> a holds not b <= a

          proof

            let L be finite Lattice;

            let X be Subset of ( LattPOSet L);

            let p be FinSequence;

            assume that

             A10: ( rng p) = X and

             A11: ( len p) = (k + 1);

            set q = (p | ( Seg k)), X9 = ( rng q);

            

             A12: ( rng q) c= ( rng p) by RELAT_1: 70;

            for x be object holds x in X9 implies x in the carrier of ( LattPOSet L)

            proof

              let x be object;

              assume x in X9;

              then x in ( rng p) by A12;

              hence thesis by A10;

            end;

            then

             A13: X9 is Subset of ( LattPOSet L) by TARSKI:def 3;

            

             A14: k <= ( len p) by A11, NAT_1: 11;

            then ( len q) = k & q <> {} by A9, CARD_1: 27, FINSEQ_1: 17;

            then

            consider a be Element of ( LattPOSet L) such that

             A15: a in X9 and

             A16: for b be Element of ( LattPOSet L) st b in X9 & b <> a holds not b <= a by A2, A13;

            consider b be set such that

             A17: (p . (k + 1)) = b;

            ( Seg (k + 1)) = ( dom p) by A11, FINSEQ_1:def 3;

            then (k + 1) in ( dom p) by FINSEQ_1: 4;

            then

             A18: b in ( rng p) by A17, FUNCT_1:def 3;

            then

            reconsider b as Element of ( LattPOSet L) by A10;

            per cases ;

              suppose ex c be Element of ( LattPOSet L) st c in X & c <= b & c <> b;

              then

              consider c be Element of ( LattPOSet L) such that

               A19: c in X and

               A20: c <= b and

               A21: c <> b;

              for u be Element of ( LattPOSet L) st u in X & u <> a holds not u <= a

              proof

                let u be Element of ( LattPOSet L);

                assume that

                 A22: u in X and

                 A23: u <> a;

                per cases ;

                  suppose u in X9;

                  hence thesis by A16, A23;

                end;

                  suppose

                   A24: not u in X9;

                  consider n be object such that

                   A25: n in ( dom p) and

                   A26: (p . n) = u by A10, A22, FUNCT_1:def 3;

                  reconsider n as Element of NAT by A25;

                  

                   A27: ( Seg (k + 1)) = ( dom p) by A11, FINSEQ_1:def 3;

                  then

                   A28: n <= (k + 1) by A25, FINSEQ_1: 1;

                  

                   A29: 1 <= n by A25, A27, FINSEQ_1: 1;

                  

                   A30: n = (k + 1)

                  proof

                    assume n <> (k + 1);

                    then n < (k + 1) by A28, XXREAL_0: 1;

                    then n <= k by NAT_1: 13;

                    then n in ( Seg k) by A29, FINSEQ_1: 1;

                    then

                     A31: n in ( dom q) by A14, FINSEQ_1: 17;

                    then (q . n) = u by A26, FUNCT_1: 47;

                    hence thesis by A24, A31, FUNCT_1:def 3;

                  end;

                  

                   A32: c in X9

                  proof

                    consider n be object such that

                     A33: n in ( dom p) and

                     A34: (p . n) = c by A10, A19, FUNCT_1:def 3;

                    reconsider n as Element of NAT by A33;

                    

                     A35: ( Seg (k + 1)) = ( dom p) by A11, FINSEQ_1:def 3;

                    then n <= (k + 1) by A33, FINSEQ_1: 1;

                    then n < (k + 1) by A17, A21, A34, XXREAL_0: 1;

                    then

                     A36: n <= k by NAT_1: 13;

                    1 <= n by A33, A35, FINSEQ_1: 1;

                    then n in ( Seg k) by A36, FINSEQ_1: 1;

                    then

                     A37: n in ( dom q) by A14, FINSEQ_1: 17;

                    then (q . n) = c by A34, FUNCT_1: 47;

                    hence thesis by A37, FUNCT_1:def 3;

                  end;

                  assume

                   A38: u <= a;

                  then c <> a by A17, A20, A21, A26, A30, ORDERS_2: 2;

                  hence thesis by A16, A17, A20, A26, A30, A38, A32, ORDERS_2: 3;

                end;

              end;

              hence thesis by A10, A12, A15;

            end;

              suppose not (ex c be Element of ( LattPOSet L) st c in X & c <= b & c <> b);

              then for u be Element of ( LattPOSet L) st u in X & u <> b holds not u <= b;

              hence thesis by A10, A18;

            end;

          end;

          hence thesis;

        end;

      end;

      

       A39: P[ 0 ]

      proof

        let L be finite Lattice;

        let X be Subset of ( LattPOSet L);

        let p be FinSequence;

        assume that

         A40: ( rng p) = X and

         A41: ( len p) = 0 ;

        ( Seg 0 ) = ( dom p) by A41, FINSEQ_1:def 3;

        hence thesis by A40, RELAT_1: 42;

      end;

      

       A42: for k be Nat holds P[k] from NAT_1:sch 2( A39, A1);

      reconsider X as finite Subset of L;

      ( LattPOSet L) = RelStr (# the carrier of L, ( LattRel L) #) by LATTICE3:def 2;

      then

      reconsider X9 = X as finite Subset of ( LattPOSet L);

      consider p be FinSequence such that

       A43: ( rng p) = X9 by FINSEQ_1: 52;

      ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

      hence thesis by A42, A43;

    end;

    

     Lm2: for L be finite Lattice holds for X be Subset of L holds X is empty or ex a be Element of ( LattPOSet L) st a in X & for b be Element of ( LattPOSet L) st b in X & b <> a holds not a <= b

    proof

      defpred P[ Nat] means for L be finite Lattice holds for X be Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X & ( len p) = $1 holds X is empty or ex a be Element of ( LattPOSet L) st a in X & for b be Element of ( LattPOSet L) st b in X & b <> a holds not (a <= b);

      let L be finite Lattice;

      let X be Subset of L;

      

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

      proof

        let k be Nat;

        assume

         A2: P[k];

        per cases ;

          suppose

           A3: k = 0 ;

          for L be finite Lattice holds for X be Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X & ( len p) = 1 holds ex a be Element of ( LattPOSet L) st a in X & for b be Element of ( LattPOSet L) st b in X & b <> a holds not a <= b

          proof

            let L be finite Lattice;

            let X be Subset of ( LattPOSet L);

            let p be FinSequence;

            assume that

             A4: ( rng p) = X and

             A5: ( len p) = 1;

            consider a be set such that

             A6: (p . 1) = a;

            

             A7: ( dom p) = {1} by A5, FINSEQ_1: 2, FINSEQ_1:def 3;

            then 1 in ( dom p) by TARSKI:def 1;

            then

             A8: a in ( rng p) by A6, FUNCT_1:def 3;

            then

            reconsider a as Element of ( LattPOSet L) by A4;

            ( rng p) = {a} by A7, A6, FUNCT_1: 4;

            then for b be Element of ( LattPOSet L) st b in X & b <> a holds not a <= b by A4, TARSKI:def 1;

            hence thesis by A4, A8;

          end;

          hence thesis by A3;

        end;

          suppose

           A9: k <> 0 ;

          for L be finite Lattice holds for X be Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X & ( len p) = (k + 1) holds ex a be Element of ( LattPOSet L) st a in X & for b be Element of ( LattPOSet L) st b in X & b <> a holds not a <= b

          proof

            let L be finite Lattice;

            let X be Subset of ( LattPOSet L);

            let p be FinSequence;

            assume that

             A10: ( rng p) = X and

             A11: ( len p) = (k + 1);

            set q = (p | ( Seg k)), X9 = ( rng q);

            

             A12: ( rng q) c= ( rng p) by RELAT_1: 70;

            for x be object holds x in X9 implies x in the carrier of ( LattPOSet L)

            proof

              let x be object;

              assume x in X9;

              then x in ( rng p) by A12;

              hence thesis by A10;

            end;

            then

             A13: X9 is Subset of ( LattPOSet L) by TARSKI:def 3;

            

             A14: k <= ( len p) by A11, NAT_1: 11;

            then ( len q) = k & q <> {} by A9, CARD_1: 27, FINSEQ_1: 17;

            then

            consider a be Element of ( LattPOSet L) such that

             A15: a in X9 and

             A16: for b be Element of ( LattPOSet L) st b in X9 & b <> a holds not a <= b by A2, A13;

            consider b be set such that

             A17: (p . (k + 1)) = b;

            ( Seg (k + 1)) = ( dom p) by A11, FINSEQ_1:def 3;

            then (k + 1) in ( dom p) by FINSEQ_1: 4;

            then

             A18: b in ( rng p) by A17, FUNCT_1:def 3;

            then

            reconsider b as Element of ( LattPOSet L) by A10;

            per cases ;

              suppose ex c be Element of ( LattPOSet L) st c in X & b <= c & c <> b;

              then

              consider c be Element of ( LattPOSet L) such that

               A19: c in X and

               A20: b <= c and

               A21: c <> b;

              for u be Element of ( LattPOSet L) st u in X & u <> a holds not a <= u

              proof

                let u be Element of ( LattPOSet L);

                assume that

                 A22: u in X and

                 A23: u <> a;

                now

                  per cases ;

                    case u in X9;

                    hence thesis by A16, A23;

                  end;

                    case

                     A24: not u in X9;

                    consider n be object such that

                     A25: n in ( dom p) and

                     A26: (p . n) = u by A10, A22, FUNCT_1:def 3;

                    reconsider n as Element of NAT by A25;

                    

                     A27: ( Seg (k + 1)) = ( dom p) by A11, FINSEQ_1:def 3;

                    then

                     A28: n <= (k + 1) by A25, FINSEQ_1: 1;

                    

                     A29: 1 <= n by A25, A27, FINSEQ_1: 1;

                    

                     A30: n = (k + 1)

                    proof

                      assume n <> (k + 1);

                      then n < (k + 1) by A28, XXREAL_0: 1;

                      then n <= k by NAT_1: 13;

                      then n in ( Seg k) by A29, FINSEQ_1: 1;

                      then

                       A31: n in ( dom q) by A14, FINSEQ_1: 17;

                      then (q . n) = u by A26, FUNCT_1: 47;

                      hence thesis by A24, A31, FUNCT_1:def 3;

                    end;

                    

                     A32: c in X9

                    proof

                      consider n be object such that

                       A33: n in ( dom p) and

                       A34: (p . n) = c by A10, A19, FUNCT_1:def 3;

                      reconsider n as Element of NAT by A33;

                      

                       A35: ( Seg (k + 1)) = ( dom p) by A11, FINSEQ_1:def 3;

                      then n <= (k + 1) by A33, FINSEQ_1: 1;

                      then n < (k + 1) by A17, A21, A34, XXREAL_0: 1;

                      then

                       A36: n <= k by NAT_1: 13;

                      1 <= n by A33, A35, FINSEQ_1: 1;

                      then n in ( Seg k) by A36, FINSEQ_1: 1;

                      then

                       A37: n in ( dom q) by A14, FINSEQ_1: 17;

                      then (q . n) = c by A34, FUNCT_1: 47;

                      hence thesis by A37, FUNCT_1:def 3;

                    end;

                    assume a <= u;

                    then c <> a by A17, A20, A21, A26, A30, ORDERS_2: 2;

                    hence thesis by A16, A17, A20, A26, A30, A32, ORDERS_2: 3;

                  end;

                end;

                hence thesis;

              end;

              hence thesis by A10, A12, A15;

            end;

              suppose not (ex c be Element of ( LattPOSet L) st c in X & b <= c & c <> b);

              then for u be Element of ( LattPOSet L) st u in X & u <> b holds not b <= u;

              hence thesis by A10, A18;

            end;

          end;

          hence thesis;

        end;

      end;

      

       A38: P[ 0 ]

      proof

        let L be finite Lattice;

        let X be Subset of ( LattPOSet L);

        let p be FinSequence;

        assume that

         A39: ( rng p) = X and

         A40: ( len p) = 0 ;

        ( Seg 0 ) = ( dom p) by A40, FINSEQ_1:def 3;

        hence thesis by A39, RELAT_1: 42;

      end;

      

       A41: for k be Nat holds P[k] from NAT_1:sch 2( A38, A1);

      reconsider X as finite Subset of L;

      ( LattPOSet L) = RelStr (# the carrier of L, ( LattRel L) #) by LATTICE3:def 2;

      then

      reconsider X9 = X as finite Subset of ( LattPOSet L);

      consider p be FinSequence such that

       A42: ( rng p) = X9 by FINSEQ_1: 52;

      ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

      hence thesis by A41, A42;

    end;

    

     Lm3: for L be finite Lattice holds for X be Subset of L holds X is empty or ex a be Element of ( LattPOSet L) st for b be Element of ( LattPOSet L) st b in X holds b <= a

    proof

      defpred P[ Nat] means for L be finite Lattice holds for X be Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X & ( len p) = $1 holds X is empty or ex a be Element of ( LattPOSet L) st for b be Element of ( LattPOSet L) st b in X holds b <= a;

      let L be finite Lattice;

      let X be Subset of L;

      

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

      proof

        let k be Nat;

        assume

         A2: P[k];

        per cases ;

          suppose

           A3: k = 0 ;

          for L be finite Lattice holds for X be Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X & ( len p) = 1 holds ex a be Element of ( LattPOSet L) st for b be Element of ( LattPOSet L) st b in X holds b <= a

          proof

            let L be finite Lattice;

            let X be Subset of ( LattPOSet L);

            let p be FinSequence;

            assume that

             A4: ( rng p) = X and

             A5: ( len p) = 1;

            consider a be set such that

             A6: (p . 1) = a;

            

             A7: ( Seg 1) = ( dom p) by A5, FINSEQ_1:def 3;

            then 1 in ( dom p) by FINSEQ_1: 2, TARSKI:def 1;

            then a in ( rng p) by A6, FUNCT_1:def 3;

            then

            reconsider a as Element of ( LattPOSet L) by A4;

            ( rng p) = {a} by A7, A6, FINSEQ_1: 2, FUNCT_1: 4;

            then for b be Element of ( LattPOSet L) st b in X holds b <= a by A4, TARSKI:def 1;

            hence thesis;

          end;

          hence thesis by A3;

        end;

          suppose

           A8: k <> 0 ;

          for L be finite Lattice holds for X be Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X & ( len p) = (k + 1) holds ex a be Element of ( LattPOSet L) st for b be Element of ( LattPOSet L) st b in X holds b <= a

          proof

            let L be finite Lattice;

            let X be Subset of ( LattPOSet L);

            let p be FinSequence;

            assume that

             A9: ( rng p) = X and

             A10: ( len p) = (k + 1);

            consider b be set such that

             A11: (p . (k + 1)) = b;

            set q = (p | ( Seg k)), X9 = ( rng q);

            for x be object holds x in X9 implies x in the carrier of ( LattPOSet L)

            proof

              let x be object;

              

               A12: ( rng q) c= ( rng p) by RELAT_1: 70;

              assume x in X9;

              then x in ( rng p) by A12;

              hence thesis by A9;

            end;

            then

             A13: X9 is Subset of ( LattPOSet L) by TARSKI:def 3;

            

             A14: k <= (k + 1) by NAT_1: 11;

            then ( len q) = k & q <> {} by A8, A10, CARD_1: 27, FINSEQ_1: 17;

            then

            consider a be Element of ( LattPOSet L) such that

             A15: for b be Element of ( LattPOSet L) st b in X9 holds b <= a by A2, A13;

            ( Seg (k + 1)) = ( dom p) by A10, FINSEQ_1:def 3;

            then (k + 1) in ( dom p) by FINSEQ_1: 4;

            then b in ( rng p) by A11, FUNCT_1:def 3;

            then

            reconsider b as Element of ( LattPOSet L) by A9;

            

             A16: (( % b) % ) = ( % b) by LATTICE3:def 3

            .= b by LATTICE3:def 4;

            set a2 = (( % a) "\/" ( % b));

            (( % a) "\/" a2) = ((( % a) "\/" ( % a)) "\/" ( % b)) by LATTICES:def 5

            .= (( % a) "\/" ( % b));

            then

             A17: ( % a) [= a2 by LATTICES:def 3;

            (( % b) "\/" a2) = ((( % b) "\/" ( % b)) "\/" ( % a)) by LATTICES:def 5

            .= (( % b) "\/" ( % a));

            then

             A18: ( % b) [= a2 by LATTICES:def 3;

            

             A19: (( % a) % ) = ( % a) by LATTICE3:def 3

            .= a by LATTICE3:def 4;

            for c be Element of ( LattPOSet L) st c in X holds c <= (a2 % )

            proof

              let c be Element of ( LattPOSet L);

              assume

               A20: c in X;

              per cases ;

                suppose c in X9;

                then

                 A21: c <= a by A15;

                a <= (a2 % ) by A17, A19, LATTICE3: 7;

                hence thesis by A21, ORDERS_2: 3;

              end;

                suppose

                 A22: not c in X9;

                consider n be object such that

                 A23: n in ( dom p) and

                 A24: c = (p . n) by A9, A20, FUNCT_1:def 3;

                reconsider n as Element of NAT by A23;

                

                 A25: n in ( Seg (k + 1)) by A10, A23, FINSEQ_1:def 3;

                

                 A26: n >= (k + 1)

                proof

                  assume not n >= (k + 1);

                  then

                   A27: n <= k by INT_1: 7;

                  1 <= n by A25, FINSEQ_1: 1;

                  then

                   A28: n in ( Seg k) by A27, FINSEQ_1: 1;

                  ( dom (p | ( Seg k))) = (( dom p) /\ ( Seg k)) by RELAT_1: 61

                  .= (( Seg (k + 1)) /\ ( Seg k)) by A10, FINSEQ_1:def 3

                  .= ( Seg k) by FINSEQ_1: 7, NAT_1: 11;

                  then

                   A29: (q . n) = c by A24, A28, FUNCT_1: 47;

                  n in ( dom q) by A10, A14, A28, FINSEQ_1: 17;

                  hence thesis by A22, A29, FUNCT_1:def 3;

                end;

                n <= (k + 1) by A25, FINSEQ_1: 1;

                then c = b by A11, A24, A26, XXREAL_0: 1;

                hence thesis by A18, A16, LATTICE3: 7;

              end;

            end;

            hence thesis;

          end;

          hence thesis;

        end;

      end;

      

       A30: P[ 0 ]

      proof

        let L be finite Lattice;

        let X be Subset of ( LattPOSet L);

        let p be FinSequence;

        assume that

         A31: ( rng p) = X and

         A32: ( len p) = 0 ;

        ( Seg ( len p)) = {} by A32;

        then ( dom p) = {} by FINSEQ_1:def 3;

        hence thesis by A31, RELAT_1: 42;

      end;

      

       A33: for k be Nat holds P[k] from NAT_1:sch 2( A30, A1);

      reconsider X as finite Subset of L;

      ( LattPOSet L) = RelStr (# the carrier of L, ( LattRel L) #) by LATTICE3:def 2;

      then

      reconsider X9 = X as finite Subset of ( LattPOSet L);

      consider p be FinSequence such that

       A34: ( rng p) = X9 by FINSEQ_1: 52;

      ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

      hence thesis by A33, A34;

    end;

    

     Lm4: for L be finite Lattice holds ex a be Element of ( LattPOSet L) st for b be Element of ( LattPOSet L) holds b <= a

    proof

      let L be finite Lattice;

      the carrier of L c= the carrier of L;

      then

      reconsider L9 = the carrier of L as Subset of L;

      consider a be Element of ( LattPOSet L) such that

       A1: for b be Element of ( LattPOSet L) st b in L9 holds b <= a by Lm3;

      for b be Element of ( LattPOSet L) holds b <= a

      proof

        let b be Element of ( LattPOSet L);

        ( LattPOSet L) = RelStr (# the carrier of L, ( LattRel L) #) by LATTICE3:def 2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    

     Lm5: for L be finite Lattice holds L is complete

    proof

      let L be finite Lattice;

      for X be Subset of L holds ex a be Element of L st a is_less_than X & for b be Element of L st b is_less_than X holds b [= a

      proof

        defpred P[ Nat] means for X9 be finite Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X9 & ( len p) = $1 holds ex a be Element of ( LattPOSet L) st (for x be Element of ( LattPOSet L) st x in X9 holds a <= x) & (for x9 be Element of ( LattPOSet L) st for x be Element of ( LattPOSet L) st x in X9 holds x9 <= x holds x9 <= a);

        let X be Subset of L;

        

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

        proof

          let k be Nat;

          assume

           A2: P[k];

          for X9 be finite Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X9 & ( len p) = (k + 1) holds ex a be Element of ( LattPOSet L) st (for x be Element of ( LattPOSet L) st x in X9 holds a <= x) & for x9 be Element of ( LattPOSet L) st for x be Element of ( LattPOSet L) st x in X9 holds x9 <= x holds x9 <= a

          proof

            let X be finite Subset of ( LattPOSet L);

            let p be FinSequence;

            assume that

             A3: ( rng p) = X and

             A4: ( len p) = (k + 1);

            set q = (p | ( Seg k)), X9 = ( rng q);

            for x be object holds x in X9 implies x in the carrier of ( LattPOSet L)

            proof

              let x be object;

              

               A5: ( rng q) c= ( rng p) by RELAT_1: 70;

              assume x in X9;

              then x in ( rng p) by A5;

              hence thesis by A3;

            end;

            then

             A6: X9 is Subset of ( LattPOSet L) by TARSKI:def 3;

            

             A7: k <= (k + 1) by NAT_1: 11;

            then ( len q) = k by A4, FINSEQ_1: 17;

            then

            consider a be Element of ( LattPOSet L) such that

             A8: for x be Element of ( LattPOSet L) st x in X9 holds a <= x and

             A9: for x9 be Element of ( LattPOSet L) st for x be Element of ( LattPOSet L) st x in X9 holds x9 <= x holds x9 <= a by A2, A6;

            consider b be set such that

             A10: (p . (k + 1)) = b;

            ( Seg (k + 1)) = ( dom p) by A4, FINSEQ_1:def 3;

            then (k + 1) in ( dom p) by FINSEQ_1: 4;

            then

             A11: b in ( rng p) by A10, FUNCT_1:def 3;

            then

            reconsider b as Element of ( LattPOSet L) by A3;

            

             A12: (( % b) % ) = ( % b) by LATTICE3:def 3

            .= b by LATTICE3:def 4;

            set a2 = (( % a) "/\" ( % b));

            (a2 "\/" ( % a)) = ( % a) by LATTICES:def 8;

            then

             A13: a2 [= ( % a) by LATTICES:def 3;

            (a2 "\/" ( % b)) = ( % b) by LATTICES:def 8;

            then

             A14: a2 [= ( % b) by LATTICES:def 3;

            

             A15: (( % a) % ) = ( % a) by LATTICE3:def 3

            .= a by LATTICE3:def 4;

            

             A16: for x be Element of ( LattPOSet L) st x in X holds (a2 % ) <= x

            proof

              let c be Element of ( LattPOSet L);

              assume

               A17: c in X;

              per cases ;

                suppose c in X9;

                then

                 A18: a <= c by A8;

                (a2 % ) <= a by A13, A15, LATTICE3: 7;

                hence thesis by A18, ORDERS_2: 3;

              end;

                suppose

                 A19: not c in X9;

                consider n be object such that

                 A20: n in ( dom p) and

                 A21: c = (p . n) by A3, A17, FUNCT_1:def 3;

                reconsider n as Element of NAT by A20;

                

                 A22: n in ( Seg (k + 1)) by A4, A20, FINSEQ_1:def 3;

                

                 A23: n >= (k + 1)

                proof

                  assume not n >= (k + 1);

                  then

                   A24: n <= k by INT_1: 7;

                  1 <= n by A22, FINSEQ_1: 1;

                  then

                   A25: n in ( Seg k) by A24, FINSEQ_1: 1;

                  ( dom (p | ( Seg k))) = (( dom p) /\ ( Seg k)) by RELAT_1: 61

                  .= (( Seg (k + 1)) /\ ( Seg k)) by A4, FINSEQ_1:def 3

                  .= ( Seg k) by FINSEQ_1: 7, NAT_1: 11;

                  then

                   A26: (q . n) = c by A21, A25, FUNCT_1: 47;

                  n in ( dom q) by A4, A7, A25, FINSEQ_1: 17;

                  hence thesis by A19, A26, FUNCT_1:def 3;

                end;

                n <= (k + 1) by A22, FINSEQ_1: 1;

                then c = b by A10, A21, A23, XXREAL_0: 1;

                hence thesis by A14, A12, LATTICE3: 7;

              end;

            end;

            for x9 be Element of ( LattPOSet L) st for x be Element of ( LattPOSet L) st x in X holds x9 <= x holds x9 <= (a2 % )

            proof

              let x9 be Element of ( LattPOSet L);

              

               A27: (( % b) % ) = ( % b) by LATTICE3:def 3

              .= b by LATTICE3:def 4;

              

               A28: (( % x9) % ) = ( % x9) by LATTICE3:def 3

              .= x9 by LATTICE3:def 4;

              assume

               A29: for x be Element of ( LattPOSet L) st x in X holds x9 <= x;

              for x be Element of ( LattPOSet L) st x in X9 holds x9 <= x

              proof

                let x be Element of ( LattPOSet L);

                ( rng q) c= ( rng p) by RELAT_1: 70;

                hence thesis by A3, A29;

              end;

              then

               A30: x9 <= a by A9;

              (( % a) % ) = ( % a) by LATTICE3:def 3

              .= a by LATTICE3:def 4;

              then

               A31: ( % x9) [= ( % a) by A30, A28, LATTICE3: 7;

              x9 <= b by A3, A11, A29;

              then

               A32: ( % x9) [= ( % b) by A27, A28, LATTICE3: 7;

              (( % x9) "/\" a2) = ((( % x9) "/\" ( % a)) "/\" ( % b)) by LATTICES:def 7

              .= (( % x9) "/\" ( % b)) by A31, LATTICES: 4

              .= ( % x9) by A32, LATTICES: 4;

              then ( % x9) [= a2 by LATTICES: 4;

              hence thesis by A28, LATTICE3: 7;

            end;

            hence thesis by A16;

          end;

          hence thesis;

        end;

        for X9 be finite Subset of ( LattPOSet L) holds for p be FinSequence st ( rng p) = X9 & ( len p) = 0 holds ex a be Element of ( LattPOSet L) st (for x be Element of ( LattPOSet L) st x in X9 holds a <= x) & for x9 be Element of ( LattPOSet L) st for x be Element of ( LattPOSet L) st x in X9 holds x9 <= x holds x9 <= a

        proof

          let X9 be finite Subset of ( LattPOSet L);

          let p be FinSequence;

          assume that

           A33: ( rng p) = X9 and

           A34: ( len p) = 0 ;

          ( Seg ( len p)) = {} by A34;

          then

           A35: ( dom p) = {} by FINSEQ_1:def 3;

          ex a be Element of ( LattPOSet L) st (for x be Element of ( LattPOSet L) st x in X9 holds a <= x) & for x9 be Element of ( LattPOSet L) st for x be Element of ( LattPOSet L) st x in X9 holds x9 <= x holds x9 <= a

          proof

            consider a be Element of ( LattPOSet L) such that

             A36: for b be Element of ( LattPOSet L) holds b <= a by Lm4;

            

             A37: for x9 be Element of ( LattPOSet L) st for x be Element of ( LattPOSet L) st x in X9 holds x9 <= x holds x9 <= a by A36;

            for x be Element of ( LattPOSet L) st x in X9 holds a <= x by A33, A35, RELAT_1: 42;

            hence thesis by A37;

          end;

          hence thesis;

        end;

        then

         A38: P[ 0 ];

        

         A39: for k be Nat holds P[k] from NAT_1:sch 2( A38, A1);

        reconsider X as finite Subset of L;

        ( LattPOSet L) = RelStr (# the carrier of L, ( LattRel L) #) by LATTICE3:def 2;

        then

        reconsider X9 = X as finite Subset of ( LattPOSet L);

        consider p be FinSequence such that

         A40: ( rng p) = X9 by FINSEQ_1: 52;

        ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        then

        consider a be Element of ( LattPOSet L) such that

         A41: for x be Element of ( LattPOSet L) st x in X9 holds a <= x and

         A42: for x9 be Element of ( LattPOSet L) st for x be Element of ( LattPOSet L) st x in X9 holds x9 <= x holds x9 <= a by A39, A40;

        

         A43: for b be Element of L st b is_less_than X holds b [= ( % a)

        proof

          let b be Element of L;

          assume

           A44: b is_less_than X;

          for x be Element of ( LattPOSet L) st x in X9 holds (b % ) <= x

          proof

            let x be Element of ( LattPOSet L);

            assume x in X9;

            then

            consider x9 be Element of L such that

             A45: x9 = x and

             A46: x9 in X;

            b [= x9 by A44, A46, LATTICE3:def 16;

            then (b % ) <= (x9 % ) by LATTICE3: 7;

            hence thesis by A45, LATTICE3:def 3;

          end;

          then

           A47: (b % ) <= a by A42;

          (( % a) % ) = ( % a) by LATTICE3:def 3

          .= a by LATTICE3:def 4;

          hence thesis by A47, LATTICE3: 7;

        end;

        for x be Element of L st x in X holds ( % a) [= x

        proof

          let x be Element of L;

          

           A48: (( % a) % ) = ( % a) by LATTICE3:def 3

          .= a by LATTICE3:def 4;

          assume x in X;

          then

          consider x9 be Element of ( LattPOSet L) such that

           A49: x9 = x & x9 in X9;

          a <= x9 & x9 = (x % ) by A41, A49, LATTICE3:def 3;

          hence thesis by A48, LATTICE3: 7;

        end;

        then ( % a) is_less_than X by LATTICE3:def 16;

        hence thesis by A43;

      end;

      hence thesis by VECTSP_8:def 6;

    end;

    registration

      cluster finite -> complete for Lattice;

      coherence by Lm5;

    end

    definition

      let L be Lattice;

      let D be Subset of L;

      :: LATTICE6:def1

      func D % -> Subset of ( LattPOSet L) equals { (d % ) where d be Element of L : d in D };

      coherence

      proof

        set M9 = { (d % ) where d be Element of L : d in D };

        for x be object holds x in M9 implies x in the carrier of ( LattPOSet L)

        proof

          let x be object;

          assume x in M9;

          then ex x9 be Element of L st x = (x9 % ) & x9 in D;

          hence thesis;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    definition

      let L be Lattice;

      let D be Subset of ( LattPOSet L);

      :: LATTICE6:def2

      func % D -> Subset of L equals { ( % d) where d be Element of ( LattPOSet L) : d in D };

      coherence

      proof

        set M9 = { ( % d) where d be Element of ( LattPOSet L) : d in D };

        for x be object holds x in M9 implies x in the carrier of L

        proof

          let x be object;

          assume x in M9;

          then ex x9 be Element of ( LattPOSet L) st x = ( % x9) & x9 in D;

          hence thesis;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let L be finite Lattice;

      cluster ( LattPOSet L) -> well_founded;

      coherence

      proof

        let Y be set;

        set R = ( LattPOSet L);

        assume that

         A1: Y c= the carrier of R and

         A2: Y <> {} ;

        ( LattPOSet L) = RelStr (# the carrier of L, ( LattRel L) #) by LATTICE3:def 2;

        then

        reconsider Y as Subset of L by A1;

        consider a be Element of ( LattPOSet L) such that

         A3: a in Y and

         A4: for b be Element of ( LattPOSet L) st b in Y & b <> a holds not b <= a by A2, Lm1;

        

         A5: not (ex x be Element of R st x <> a & [x, a] in the InternalRel of R & x in Y) by ORDERS_2:def 5, A4;

        ((the InternalRel of R -Seg a) /\ Y) = {}

        proof

          set z = the Element of ((the InternalRel of R -Seg a) /\ Y);

          assume

           A6: ((the InternalRel of R -Seg a) /\ Y) <> {} ;

          then z in (the InternalRel of R -Seg a) by XBOOLE_0:def 4;

          then

           A7: z <> a & [z, a] in the InternalRel of R by WELLORD1: 1;

          z in Y by A6, XBOOLE_0:def 4;

          hence thesis by A1, A5, A7;

        end;

        then (the InternalRel of R -Seg a) misses Y by XBOOLE_0:def 7;

        hence thesis by A3;

      end;

    end

    

     Lm6: for L be finite Lattice holds (( LattPOSet L) ~ ) is well_founded

    proof

      let L be finite Lattice;

      set R = ( LattPOSet L);

      

       A1: (( LattPOSet L) ~ ) = RelStr (# the carrier of R, (the InternalRel of R ~ ) #) by LATTICE3:def 5;

      for Y be set st Y c= the carrier of (R ~ ) & Y <> {} holds ex a be object st a in Y & (the InternalRel of (R ~ ) -Seg a) misses Y

      proof

        let Y be set;

        assume that

         A2: Y c= the carrier of (R ~ ) and

         A3: Y <> {} ;

        ( LattPOSet L) = RelStr (# the carrier of L, ( LattRel L) #) by LATTICE3:def 2;

        then

        reconsider Y as Subset of L by A1, A2;

        consider a be Element of R such that

         A4: a in Y and

         A5: for b be Element of ( LattPOSet L) st b in Y & b <> a holds not a <= b by A3, Lm2;

        reconsider a as Element of R;

        reconsider a9 = a as Element of (R ~ ) by A1;

        

         A6: for b be Element of (( LattPOSet L) ~ ) st b in Y & b <> a holds not b <= a9

        proof

          let b be Element of (( LattPOSet L) ~ );

          reconsider b9 = b as Element of R by A1;

          assume b in Y & b <> a;

          then

           A7: not a <= b9 by A5;

          (a ~ ) = a9 & (b9 ~ ) = b by LATTICE3:def 6;

          hence thesis by A7, LATTICE3: 9;

        end;

        

         A8: not (ex x be Element of (R ~ ) st x <> a & [x, a] in the InternalRel of (R ~ ) & x in Y) by ORDERS_2:def 5, A6;

        ((the InternalRel of (R ~ ) -Seg a) /\ Y) = {}

        proof

          set z = the Element of ((the InternalRel of (R ~ ) -Seg a) /\ Y);

          assume

           A9: ((the InternalRel of (R ~ ) -Seg a) /\ Y) <> {} ;

          then z in (the InternalRel of (R ~ ) -Seg a) by XBOOLE_0:def 4;

          then

           A10: z <> a & [z, a] in the InternalRel of (R ~ ) by WELLORD1: 1;

          z in Y by A9, XBOOLE_0:def 4;

          hence thesis by A2, A8, A10;

        end;

        then (the InternalRel of (R ~ ) -Seg a) misses Y by XBOOLE_0:def 7;

        hence thesis by A4;

      end;

      then the InternalRel of (R ~ ) is_well_founded_in the carrier of (R ~ );

      hence thesis;

    end;

    definition

      let L be Lattice;

      :: LATTICE6:def3

      attr L is noetherian means

      : Def3: ( LattPOSet L) is well_founded;

      :: LATTICE6:def4

      attr L is co-noetherian means

      : Def4: (( LattPOSet L) ~ ) is well_founded;

    end

    registration

      cluster noetherian upper-bounded lower-bounded complete for Lattice;

      existence

      proof

        set L = the finite Lattice;

        take L;

        thus thesis;

      end;

    end

    registration

      cluster co-noetherian upper-bounded lower-bounded complete for Lattice;

      existence

      proof

        set L = the finite Lattice;

        take L;

        (( LattPOSet L) ~ ) is well_founded by Lm6;

        hence thesis;

      end;

    end

    theorem :: LATTICE6:1

    for L be Lattice holds L is noetherian iff (L .: ) is co-noetherian

    proof

      let L be Lattice;

      set R = ( LattPOSet L);

      set Ri = (( LattPOSet L) ~ );

       A1:

      now

        

         A2: (( LattPOSet L) ~ ) = ( LattPOSet (L .: )) by LATTICE3: 20;

        assume (L .: ) is co-noetherian;

        then (Ri ~ ) is well_founded by A2;

        then R is well_founded by LATTICE3: 8;

        hence L is noetherian;

      end;

      now

        assume L is noetherian;

        then R is well_founded;

        then

         A3: (Ri ~ ) is well_founded by LATTICE3: 8;

        (( LattPOSet L) ~ ) = ( LattPOSet (L .: )) by LATTICE3: 20;

        hence (L .: ) is co-noetherian by A3;

      end;

      hence thesis by A1;

    end;

    

     Lm7: for L be finite Lattice holds L is noetherian & L is co-noetherian by Lm6;

    registration

      cluster finite -> noetherian for Lattice;

      coherence ;

      cluster finite -> co-noetherian for Lattice;

      coherence by Lm7;

    end

    definition

      let L be Lattice;

      let a,b be Element of L;

      :: LATTICE6:def5

      pred a is-upper-neighbour-of b means a <> b & b [= a & for c be Element of L holds b [= c & c [= a implies (c = a or c = b);

    end

    notation

      let L be Lattice;

      let a,b be Element of L;

      synonym b is-lower-neighbour-of a for a is-upper-neighbour-of b;

    end

    theorem :: LATTICE6:2

    

     Th2: for L be Lattice holds for a be Element of L holds for b,c be Element of L st b <> c holds (b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = (c "/\" b)) & (b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = (c "\/" b))

    proof

      let L be Lattice;

      let a be Element of L;

      let b,c be Element of L;

      assume

       A1: b <> c;

       A2:

      now

        assume that

         A3: b is-lower-neighbour-of a and

         A4: c is-lower-neighbour-of a;

        

         A5: b [= a by A3;

        

         A6: c [= a by A4;

        

         A7: not (b "\/" c) = c

        proof

          assume (b "\/" c) = c;

          then b [= c by LATTICES:def 3;

          then c = a or c = b by A3, A6;

          hence contradiction by A1, A4;

        end;

        a = (a "\/" a)

        .= ((b "\/" a) "\/" a) by A5, LATTICES:def 3

        .= ((b "\/" a) "\/" (c "\/" a)) by A6, LATTICES:def 3

        .= (b "\/" (a "\/" (a "\/" c))) by LATTICES:def 5

        .= (b "\/" ((a "\/" a) "\/" c)) by LATTICES:def 5

        .= (b "\/" (a "\/" c))

        .= ((b "\/" c) "\/" a) by LATTICES:def 5;

        then

         A8: (b "\/" c) [= a by LATTICES:def 3;

        c [= (b "\/" c) by LATTICES: 5;

        hence (b "\/" c) = a by A4, A8, A7;

      end;

      now

        assume that

         A9: b is-upper-neighbour-of a and

         A10: c is-upper-neighbour-of a;

        

         A11: a [= b by A9;

        

         A12: a [= c by A10;

        

         A13: not (b "/\" c) = c

        proof

          assume (b "/\" c) = c;

          then c [= b by LATTICES: 4;

          then c = a or c = b by A9, A12;

          hence contradiction by A1, A10;

        end;

        a = (a "/\" a)

        .= ((b "/\" a) "/\" a) by A11, LATTICES: 4

        .= ((b "/\" a) "/\" (c "/\" a)) by A12, LATTICES: 4

        .= (b "/\" (a "/\" (c "/\" a))) by LATTICES:def 7

        .= (b "/\" ((a "/\" a) "/\" c)) by LATTICES:def 7

        .= (b "/\" (a "/\" c))

        .= ((b "/\" c) "/\" a) by LATTICES:def 7;

        then

         A14: a [= (b "/\" c) by LATTICES: 4;

        (b "/\" c) [= c by LATTICES: 6;

        hence (b "/\" c) = a by A10, A14, A13;

      end;

      hence thesis by A2;

    end;

    theorem :: LATTICE6:3

    

     Th3: for L be noetherian Lattice holds for a be Element of L holds for d be Element of L st a [= d & a <> d holds ex c be Element of L st c [= d & c is-upper-neighbour-of a

    proof

      let L be noetherian Lattice;

      let a be Element of L;

      let d be Element of L;

      defpred P[ Element of ( LattPOSet L)] means a [= ( % $1) & a <> ( % $1) implies ex c be Element of L st c [= ( % $1) & c is-upper-neighbour-of a;

      

       A1: ( % (d % )) = (d % ) by LATTICE3:def 4

      .= d by LATTICE3:def 3;

      

       A2: for x be Element of ( LattPOSet L) st for y be Element of ( LattPOSet L) st y <> x & [y, x] in the InternalRel of ( LattPOSet L) holds P[y] holds P[x]

      proof

        let x be Element of ( LattPOSet L);

        assume

         A3: for y be Element of ( LattPOSet L) st y <> x & [y, x] in the InternalRel of ( LattPOSet L) holds P[y];

        a [= ( % x) & a <> ( % x) implies ex c be Element of L st c [= ( % x) & c is-upper-neighbour-of a

        proof

          

           A4: (( % x) % ) = ( % x) by LATTICE3:def 3

          .= x by LATTICE3:def 4;

          assume

           A5: a [= ( % x) & a <> ( % x);

          per cases ;

            suppose ( % x) is-upper-neighbour-of a;

            hence thesis;

          end;

            suppose not ( % x) is-upper-neighbour-of a;

            then

            consider c be Element of L such that

             A6: a [= c and

             A7: c [= ( % x) and

             A8: ( not c = ( % x)) & not c = a by A5;

            (c % ) <= x by A4, A7, LATTICE3: 7;

            then

             A9: [(c % ), x] in the InternalRel of ( LattPOSet L) by ORDERS_2:def 5;

            ( % (c % )) = (c % ) by LATTICE3:def 4

            .= c by LATTICE3:def 3;

            then ex c9 be Element of L st c9 [= c & c9 is-upper-neighbour-of a by A3, A6, A8, A9;

            hence thesis by A7, LATTICES: 7;

          end;

        end;

        hence thesis;

      end;

      

       A10: ( LattPOSet L) is well_founded by Def3;

      

       A11: for x be Element of ( LattPOSet L) holds P[x] from WELLFND1:sch 3( A2, A10);

      assume a [= d & a <> d;

      hence thesis by A11, A1;

    end;

    theorem :: LATTICE6:4

    

     Th4: for L be co-noetherian Lattice holds for a be Element of L holds for d be Element of L st d [= a & a <> d holds ex c be Element of L st d [= c & c is-lower-neighbour-of a

    proof

      let L be co-noetherian Lattice;

      let a be Element of L;

      let d be Element of L;

      defpred P[ Element of (( LattPOSet L) ~ )] means ( % ( ~ $1)) [= a & a <> ( % ( ~ $1)) implies ex c be Element of L st ( % ( ~ $1)) [= c & c is-lower-neighbour-of a;

      

       A1: ( % ( ~ ((d % ) ~ ))) = ( ~ ((d % ) ~ )) by LATTICE3:def 4

      .= ((d % ) ~ ) by LATTICE3:def 7

      .= (d % ) by LATTICE3:def 6

      .= d by LATTICE3:def 3;

      

       A2: for x be Element of (( LattPOSet L) ~ ) st for y be Element of (( LattPOSet L) ~ ) st y <> x & [y, x] in the InternalRel of (( LattPOSet L) ~ ) holds P[y] holds P[x]

      proof

        let x be Element of (( LattPOSet L) ~ );

        assume

         A3: for y be Element of (( LattPOSet L) ~ ) st y <> x & [y, x] in the InternalRel of (( LattPOSet L) ~ ) holds P[y];

        ( % ( ~ x)) [= a & a <> ( % ( ~ x)) implies ex c be Element of L st ( % ( ~ x)) [= c & c is-lower-neighbour-of a

        proof

          

           A4: (( ~ x) ~ ) = ( ~ x) by LATTICE3:def 6

          .= x by LATTICE3:def 7;

          

           A5: (( % ( ~ x)) % ) = ( % ( ~ x)) by LATTICE3:def 3

          .= ( ~ x) by LATTICE3:def 4;

          assume

           A6: ( % ( ~ x)) [= a & a <> ( % ( ~ x));

          per cases ;

            suppose ( % ( ~ x)) is-lower-neighbour-of a;

            hence thesis;

          end;

            suppose not ( % ( ~ x)) is-lower-neighbour-of a;

            then

            consider c be Element of L such that

             A7: ( % ( ~ x)) [= c and

             A8: c [= a & not c = a & not c = ( % ( ~ x)) by A6;

            

             A9: ( % ( ~ ((c % ) ~ ))) = ( ~ ((c % ) ~ )) by LATTICE3:def 4

            .= ((c % ) ~ ) by LATTICE3:def 7

            .= (c % ) by LATTICE3:def 6

            .= c by LATTICE3:def 3;

            ( ~ x) <= (c % ) by A5, A7, LATTICE3: 7;

            then ((c % ) ~ ) <= x by A4, LATTICE3: 9;

            then [((c % ) ~ ), x] in the InternalRel of (( LattPOSet L) ~ ) by ORDERS_2:def 5;

            then ex c9 be Element of L st ( % ( ~ ((c % ) ~ ))) [= c9 & c9 is-lower-neighbour-of a by A3, A8, A9;

            hence thesis by A7, A9, LATTICES: 7;

          end;

        end;

        hence thesis;

      end;

      

       A10: (( LattPOSet L) ~ ) is well_founded by Def4;

      

       A11: for x be Element of (( LattPOSet L) ~ ) holds P[x] from WELLFND1:sch 3( A2, A10);

      assume d [= a & a <> d;

      hence thesis by A11, A1;

    end;

    theorem :: LATTICE6:5

    

     Th5: for L be upper-bounded Lattice holds not (ex b be Element of L st b is-upper-neighbour-of ( Top L))

    proof

      let L be upper-bounded Lattice;

      given b be Element of L such that

       A1: b is-upper-neighbour-of ( Top L);

      

       A2: b [= ( Top L) by LATTICES: 19;

      ( Top L) [= b & ( Top L) <> b by A1;

      hence thesis by A2, LATTICES: 8;

    end;

    theorem :: LATTICE6:6

    

     Th6: for L be noetherian upper-bounded Lattice holds for a be Element of L holds a = ( Top L) iff not (ex b be Element of L st b is-upper-neighbour-of a)

    proof

      let L be noetherian upper-bounded Lattice;

      let a be Element of L;

      now

        assume

         A1: not (ex b be Element of L st b is-upper-neighbour-of a);

        for b be Element of L holds (a "\/" b) = a & (b "\/" a) = a

        proof

          let b be Element of L;

          consider c be Element of L such that

           A2: c = (a "\/" b);

          

           A3: a [= c by A2, LATTICES: 5;

          per cases ;

            suppose a <> c;

            then ex d be Element of L st d [= c & d is-upper-neighbour-of a by A3, Th3;

            hence thesis by A1;

          end;

            suppose a = c;

            hence thesis by A2;

          end;

        end;

        hence a = ( Top L) by LATTICES:def 17;

      end;

      hence thesis by Th5;

    end;

    theorem :: LATTICE6:7

    

     Th7: for L be lower-bounded Lattice holds not (ex b be Element of L st b is-lower-neighbour-of ( Bottom L))

    proof

      let L be lower-bounded Lattice;

      given b be Element of L such that

       A1: b is-lower-neighbour-of ( Bottom L);

      

       A2: ( Bottom L) [= b by LATTICES: 16;

      b [= ( Bottom L) & b <> ( Bottom L) by A1;

      hence thesis by A2, LATTICES: 8;

    end;

    theorem :: LATTICE6:8

    

     Th8: for L be co-noetherian lower-bounded Lattice holds for a be Element of L holds a = ( Bottom L) iff not (ex b be Element of L st b is-lower-neighbour-of a)

    proof

      let L be co-noetherian lower-bounded Lattice;

      let a be Element of L;

      now

        assume

         A1: not (ex b be Element of L st b is-lower-neighbour-of a);

        for b be Element of L holds (a "/\" b) = a & (b "/\" a) = a

        proof

          let b be Element of L;

          consider c be Element of L such that

           A2: c = (a "/\" b);

          

           A3: c [= a by A2, LATTICES: 6;

          per cases ;

            suppose a <> c;

            then ex d be Element of L st c [= d & d is-lower-neighbour-of a by A3, Th4;

            hence thesis by A1;

          end;

            suppose a = c;

            hence thesis by A2;

          end;

        end;

        hence a = ( Bottom L) by LATTICES:def 16;

      end;

      hence thesis by Th7;

    end;

    definition

      let L be complete Lattice;

      let a be Element of L;

      :: LATTICE6:def6

      func a *' -> Element of L equals ( "/\" ({ d where d be Element of L : a [= d & d <> a },L));

      correctness ;

      :: LATTICE6:def7

      func *' a -> Element of L equals ( "\/" ({ d where d be Element of L : d [= a & d <> a },L));

      correctness ;

    end

    definition

      let L be complete Lattice;

      let a be Element of L;

      :: LATTICE6:def8

      attr a is completely-meet-irreducible means (a *' ) <> a;

      :: LATTICE6:def9

      attr a is completely-join-irreducible means ( *' a) <> a;

    end

    theorem :: LATTICE6:9

    

     Th9: for L be complete Lattice holds for a be Element of L holds a [= (a *' ) & ( *' a) [= a

    proof

      let L be complete Lattice;

      let a be Element of L;

      set X = { d where d be Element of L : a [= d & d <> a };

      for q be Element of L st q in X holds a [= q

      proof

        let q be Element of L;

        assume q in X;

        then ex q9 be Element of L st q9 = q & a [= q9 & q9 <> a;

        hence thesis;

      end;

      then

       A1: a is_less_than X by LATTICE3:def 16;

      set X = { d where d be Element of L : d [= a & d <> a };

      for q be Element of L st q in X holds q [= a

      proof

        let q be Element of L;

        assume q in X;

        then ex q9 be Element of L st q9 = q & q9 [= a & q9 <> a;

        hence thesis;

      end;

      then X is_less_than a by LATTICE3:def 17;

      hence thesis by A1, LATTICE3: 34, LATTICE3:def 21;

    end;

    theorem :: LATTICE6:10

    for L be complete Lattice holds (( Top L) *' ) = ( Top L) & (( Top L) % ) is meet-irreducible

    proof

      let L be complete Lattice;

      set X = { d where d be Element of L : ( Top L) [= d & d <> ( Top L) };

      

       A1: X = {}

      proof

        assume X <> {} ;

        then

        reconsider X as non empty set;

        set x = the Element of X;

        x in X;

        then

        consider x9 be Element of L such that x9 = x and

         A2: ( Top L) [= x9 & x9 <> ( Top L);

        x9 [= ( Top L) by LATTICES: 19;

        hence thesis by A2, LATTICES: 8;

      end;

      

       A3: for b be Element of L st b is_less_than {} holds b [= ( Top L) by LATTICES: 19;

      for q be Element of L st q in {} holds ( Top L) [= q;

      then

       A4: ( Top L) is_less_than {} by LATTICE3:def 16;

      ( Top ( LattPOSet L)) = ( "/\" ( {} ,( LattPOSet L))) by YELLOW_0:def 12

      .= ( "/\" ( {} ,L)) by YELLOW_0: 29

      .= ( Top L) by A4, A3, LATTICE3: 34;

      then (( Top L) % ) = ( Top ( LattPOSet L)) by LATTICE3:def 3;

      hence thesis by A1, A4, A3, LATTICE3: 34, WAYBEL_6: 10;

    end;

    theorem :: LATTICE6:11

    for L be complete Lattice holds ( *' ( Bottom L)) = ( Bottom L) & (( Bottom L) % ) is join-irreducible

    proof

      let L be complete Lattice;

      set X = { d where d be Element of L : d [= ( Bottom L) & d <> ( Bottom L) };

      

       A1: X = {}

      proof

        assume X <> {} ;

        then

        reconsider X as non empty set;

        set x = the Element of X;

        x in X;

        then

        consider x9 be Element of L such that x9 = x and

         A2: x9 [= ( Bottom L) & x9 <> ( Bottom L);

        ( Bottom L) [= x9 by LATTICES: 16;

        hence thesis by A2, LATTICES: 8;

      end;

      

       A3: for b be Element of L st b is_greater_than {} holds ( Bottom L) [= b by LATTICES: 16;

      

       A4: for x,y be Element of ( LattPOSet L) st ( Bottom ( LattPOSet L)) = (x "\/" y) holds x = ( Bottom ( LattPOSet L)) or y = ( Bottom ( LattPOSet L))

      proof

        reconsider L9 = ( LattPOSet L) as lower-bounded antisymmetric non empty RelStr;

        let x,y be Element of ( LattPOSet L);

        reconsider x9 = x as Element of L9;

        reconsider y9 = y as Element of L9;

        assume ( Bottom ( LattPOSet L)) = (x "\/" y);

        then

         A5: ( Bottom ( LattPOSet L)) >= x & ( Bottom ( LattPOSet L)) >= y by YELLOW_0: 22;

        x9 >= ( Bottom L9) or y9 >= ( Bottom L9) by YELLOW_0: 44;

        hence thesis by A5, ORDERS_2: 2;

      end;

      for q be Element of L st q in {} holds q [= ( Bottom L);

      then

       A6: ( Bottom L) is_greater_than {} by LATTICE3:def 17;

      ( Bottom ( LattPOSet L)) = ( "\/" ( {} ,( LattPOSet L))) by YELLOW_0:def 11

      .= ( "\/" ( {} ,L)) by YELLOW_0: 29

      .= ( Bottom L) by A6, A3, LATTICE3:def 21;

      then (( Bottom L) % ) = ( Bottom ( LattPOSet L)) by LATTICE3:def 3;

      hence thesis by A1, A6, A3, A4, LATTICE3:def 21, WAYBEL_6:def 3;

    end;

    theorem :: LATTICE6:12

    

     Th12: for L be complete Lattice holds for a be Element of L st a is completely-meet-irreducible holds (a *' ) is-upper-neighbour-of a & for c be Element of L holds c is-upper-neighbour-of a implies c = (a *' )

    proof

      let L be complete Lattice;

      let a be Element of L;

      set X = { x where x be Element of L : a [= x & x <> a };

      for c be Element of L st a [= c & c [= (a *' ) holds c = a or c = (a *' )

      proof

        let c be Element of L;

        assume that

         A1: a [= c and

         A2: c [= (a *' );

        assume c <> a;

        then c in X by A1;

        then (a *' ) [= c by LATTICE3: 38;

        hence thesis by A2, LATTICES: 8;

      end;

      then

       A3: for c be Element of L holds a [= c & c [= (a *' ) implies (c = (a *' ) or c = a);

      assume a is completely-meet-irreducible;

      then

       A4: (a *' ) <> a;

      

       A5: for c be Element of L holds c is-upper-neighbour-of a implies c = (a *' )

      proof

        let c be Element of L;

        assume

         A6: c is-upper-neighbour-of a;

        then a <> c & a [= c;

        then c in X;

        then

         A7: (a *' ) [= c by LATTICE3: 38;

        a [= (a *' ) by Th9;

        hence thesis by A4, A6, A7;

      end;

      a [= (a *' ) by Th9;

      hence thesis by A4, A3, A5;

    end;

    theorem :: LATTICE6:13

    

     Th13: for L be complete Lattice holds for a be Element of L st a is completely-join-irreducible holds ( *' a) is-lower-neighbour-of a & for c be Element of L holds c is-lower-neighbour-of a implies c = ( *' a)

    proof

      let L be complete Lattice;

      let a be Element of L;

      set X = { x where x be Element of L : x [= a & x <> a };

      

       A1: for c be Element of L st ( *' a) [= c & c [= a holds c = a or c = ( *' a)

      proof

        let c be Element of L;

        assume that

         A2: ( *' a) [= c and

         A3: c [= a;

        assume c <> a;

        then c in X by A3;

        then c [= ( *' a) by LATTICE3: 38;

        hence thesis by A2, LATTICES: 8;

      end;

      assume a is completely-join-irreducible;

      then

       A4: ( *' a) <> a;

      

       A5: for c be Element of L holds c is-lower-neighbour-of a implies c = ( *' a)

      proof

        let c be Element of L;

        assume

         A6: c is-lower-neighbour-of a;

        then a <> c & c [= a;

        then c in X;

        then

         A7: c [= ( *' a) by LATTICE3: 38;

        ( *' a) [= a by Th9;

        hence thesis by A4, A6, A7;

      end;

      ( *' a) [= a by Th9;

      hence thesis by A4, A1, A5;

    end;

    theorem :: LATTICE6:14

    

     Th14: for L be noetherian complete Lattice holds for a be Element of L holds a is completely-meet-irreducible iff ex b be Element of L st b is-upper-neighbour-of a & for c be Element of L holds c is-upper-neighbour-of a implies c = b

    proof

      let L be noetherian complete Lattice;

      let a be Element of L;

      set X = { x where x be Element of L : a [= x & x <> a };

      hereby

        assume a is completely-meet-irreducible;

        then (a *' ) is-upper-neighbour-of a & for c be Element of L holds c is-upper-neighbour-of a implies c = (a *' ) by Th12;

        hence ex b be Element of L st b is-upper-neighbour-of a & for c be Element of L holds c is-upper-neighbour-of a implies c = b;

      end;

      given b be Element of L such that

       A1: b is-upper-neighbour-of a and

       A2: for c be Element of L holds c is-upper-neighbour-of a implies c = b;

      

       A3: a <> b by A1;

      for q be Element of L st q in X holds b [= q

      proof

        let q be Element of L;

        assume q in X;

        then ex q9 be Element of L st q9 = q & a [= q9 & q9 <> a;

        then ex c be Element of L st c [= q & c is-upper-neighbour-of a by Th3;

        hence thesis by A2;

      end;

      then

       A4: b is_less_than X by LATTICE3:def 16;

      a [= b by A1;

      then b in X by A3;

      hence a <> (a *' ) by A3, A4, LATTICE3: 41;

    end;

    theorem :: LATTICE6:15

    

     Th15: for L be co-noetherian complete Lattice holds for a be Element of L holds a is completely-join-irreducible iff ex b be Element of L st b is-lower-neighbour-of a & for c be Element of L holds c is-lower-neighbour-of a implies c = b

    proof

      let L be co-noetherian complete Lattice;

      let a be Element of L;

      set X = { x where x be Element of L : x [= a & x <> a };

       A1:

      now

        given b be Element of L such that

         A2: b is-lower-neighbour-of a and

         A3: for c be Element of L holds c is-lower-neighbour-of a implies c = b;

        

         A4: a <> b by A2;

        for q be Element of L st q in X holds q [= b

        proof

          let q be Element of L;

          assume q in X;

          then ex q9 be Element of L st q9 = q & q9 [= a & q9 <> a;

          then ex c be Element of L st q [= c & c is-lower-neighbour-of a by Th4;

          hence thesis by A3;

        end;

        then

         A5: b is_greater_than X by LATTICE3:def 17;

        b [= a by A2;

        then b in X by A4;

        then a <> ( *' a) by A4, A5, LATTICE3: 40;

        hence a is completely-join-irreducible;

      end;

      now

        assume a is completely-join-irreducible;

        then ( *' a) is-lower-neighbour-of a & for c be Element of L holds c is-lower-neighbour-of a implies c = ( *' a) by Th13;

        hence ex b be Element of L st b is-lower-neighbour-of a & for c be Element of L holds c is-lower-neighbour-of a implies c = b;

      end;

      hence thesis by A1;

    end;

    theorem :: LATTICE6:16

    

     Th16: for L be complete Lattice holds for a be Element of L holds a is completely-meet-irreducible implies (a % ) is meet-irreducible

    proof

      let L be complete Lattice;

      let a be Element of L;

      set X = { d where d be Element of L : a [= d & d <> a };

      assume a is completely-meet-irreducible;

      then

       A1: a <> (a *' );

      for x,y be Element of ( LattPOSet L) st (a % ) = (x "/\" y) holds x = (a % ) or y = (a % )

      proof

        a [= (a *' ) by Th9;

        then

         A2: (a % ) <= ((a *' ) % ) by LATTICE3: 7;

        

         A3: ( % (a % )) = (a % ) by LATTICE3:def 4;

        

         A4: a = (a % ) & (a *' ) = ((a *' ) % ) by LATTICE3:def 3;

        

         A5: (a *' ) is_less_than X by LATTICE3: 34;

        let x,y be Element of ( LattPOSet L);

        

         A6: a = (a % ) by LATTICE3:def 3

        .= ( % (a % )) by LATTICE3:def 4;

        

         A7: x = ( % x) by LATTICE3:def 4

        .= (( % x) % ) by LATTICE3:def 3;

        assume

         A8: (a % ) = (x "/\" y);

        then (a % ) <= x by YELLOW_0: 23;

        then

         A9: a [= ( % x) by A7, LATTICE3: 7;

        assume that

         A10: x <> (a % ) and

         A11: y <> (a % );

        

         A12: y = ( % y) by LATTICE3:def 4

        .= (( % y) % ) by LATTICE3:def 3;

        (a % ) <= y by A8, YELLOW_0: 23;

        then

         A13: a [= ( % y) by A12, LATTICE3: 7;

        y = ( % y) by LATTICE3:def 4;

        then ( % y) in X by A6, A13, A3, A11;

        then (a *' ) [= ( % y) by A5, LATTICE3:def 16;

        then

         A14: ((a *' ) % ) <= (( % y) % ) by LATTICE3: 7;

        x = ( % x) by LATTICE3:def 4;

        then ( % x) in X by A6, A9, A3, A10;

        then (a *' ) [= ( % x) by A5, LATTICE3:def 16;

        then ((a *' ) % ) <= (( % x) % ) by LATTICE3: 7;

        then ((a *' ) % ) <= (a % ) by A8, A12, A7, A14, YELLOW_0: 23;

        hence contradiction by A1, A2, A4, ORDERS_2: 2;

      end;

      hence thesis by WAYBEL_6:def 2;

    end;

    

     Lm8: for L be Lattice holds for a,b be Element of L holds (a "/\" b) = ((a % ) "/\" (b % )) & (a "\/" b) = ((a % ) "\/" (b % ))

    proof

      let L be Lattice;

      let a,b be Element of L;

      consider c be Element of L such that

       A1: c = (a "/\" b);

      

       A2: for d be Element of ( LattPOSet L) st d <= (a % ) & d <= (b % ) holds (c % ) >= d

      proof

        let d be Element of ( LattPOSet L);

        assume that

         A3: d <= (a % ) and

         A4: d <= (b % );

        

         A5: (( % d) % ) = ( % d) by LATTICE3:def 3

        .= d by LATTICE3:def 4;

        then

         A6: ( % d) [= a by A3, LATTICE3: 7;

        

         A7: ( % d) [= b by A4, A5, LATTICE3: 7;

        (( % d) "/\" c) = ((( % d) "/\" a) "/\" b) by A1, LATTICES:def 7

        .= (( % d) "/\" b) by A6, LATTICES: 4

        .= ( % d) by A7, LATTICES: 4;

        then ( % d) [= c by LATTICES: 4;

        hence thesis by A5, LATTICE3: 7;

      end;

      c [= b by A1, LATTICES: 6;

      then

       A8: (c % ) <= (b % ) by LATTICE3: 7;

      c [= a by A1, LATTICES: 6;

      then (c % ) <= (a % ) by LATTICE3: 7;

      then

       A9: (c % ) = ((a % ) "/\" (b % )) by A8, A2, YELLOW_0: 23;

      consider c be Element of L such that

       A10: c = (a "\/" b);

      

       A11: for d be Element of ( LattPOSet L) st (a % ) <= d & (b % ) <= d holds d >= (c % )

      proof

        let d be Element of ( LattPOSet L);

        assume that

         A12: (a % ) <= d and

         A13: (b % ) <= d;

        

         A14: (( % d) % ) = ( % d) by LATTICE3:def 3

        .= d by LATTICE3:def 4;

        then

         A15: a [= ( % d) by A12, LATTICE3: 7;

        

         A16: b [= ( % d) by A13, A14, LATTICE3: 7;

        (( % d) "\/" c) = ((( % d) "\/" a) "\/" b) by A10, LATTICES:def 5

        .= (( % d) "\/" b) by A15, LATTICES:def 3

        .= ( % d) by A16, LATTICES:def 3;

        then c [= ( % d) by LATTICES:def 3;

        hence thesis by A14, LATTICE3: 7;

      end;

      b [= c by A10, LATTICES: 5;

      then

       A17: (b % ) <= (c % ) by LATTICE3: 7;

      a [= c by A10, LATTICES: 5;

      then (a % ) <= (c % ) by LATTICE3: 7;

      then (c % ) = ((a % ) "\/" (b % )) by A17, A11, YELLOW_0: 22;

      hence thesis by A1, A9, A10, LATTICE3:def 3;

    end;

    theorem :: LATTICE6:17

    

     Th17: for L be complete noetherian Lattice holds for a be Element of L st a <> ( Top L) holds a is completely-meet-irreducible iff (a % ) is meet-irreducible

    proof

      let L be complete noetherian Lattice;

      let a be Element of L;

      assume a <> ( Top L);

      then

      consider b be Element of L such that

       A1: b is-upper-neighbour-of a by Th6;

      

       A2: b <> a by A1;

      now

        assume

         A3: (a % ) is meet-irreducible;

        for d be Element of L holds d is-upper-neighbour-of a implies d = b

        proof

          let d be Element of L;

          

           A4: (a % ) = a by LATTICE3:def 3;

          

           A5: (d % ) = d & (b % ) = b by LATTICE3:def 3;

          assume

           A6: d is-upper-neighbour-of a;

          then

           A7: d <> a;

          assume d <> b;

          then a = (d "/\" b) by A1, A6, Th2;

          then (a % ) = ((d % ) "/\" (b % )) by A4, Lm8;

          hence thesis by A2, A3, A7, A4, A5, WAYBEL_6:def 2;

        end;

        hence a is completely-meet-irreducible by A1, Th14;

      end;

      hence thesis by Th16;

    end;

    theorem :: LATTICE6:18

    

     Th18: for L be complete Lattice holds for a be Element of L holds a is completely-join-irreducible implies (a % ) is join-irreducible

    proof

      let L be complete Lattice;

      let a be Element of L;

      set X = { d where d be Element of L : d [= a & d <> a };

      assume a is completely-join-irreducible;

      then

       A1: a <> ( *' a);

      for x,y be Element of ( LattPOSet L) st (a % ) = (x "\/" y) holds x = (a % ) or y = (a % )

      proof

        ( *' a) [= a by Th9;

        then

         A2: (a % ) >= (( *' a) % ) by LATTICE3: 7;

        

         A3: ( % (a % )) = (a % ) by LATTICE3:def 4;

        

         A4: a = (a % ) & ( *' a) = (( *' a) % ) by LATTICE3:def 3;

        

         A5: X is_less_than ( *' a) by LATTICE3:def 21;

        let x,y be Element of ( LattPOSet L);

        

         A6: a = (a % ) by LATTICE3:def 3

        .= ( % (a % )) by LATTICE3:def 4;

        

         A7: x = ( % x) by LATTICE3:def 4

        .= (( % x) % ) by LATTICE3:def 3;

        assume

         A8: (a % ) = (x "\/" y);

        then x <= (a % ) by YELLOW_0: 22;

        then

         A9: ( % x) [= a by A7, LATTICE3: 7;

        assume that

         A10: x <> (a % ) and

         A11: y <> (a % );

        

         A12: y = ( % y) by LATTICE3:def 4

        .= (( % y) % ) by LATTICE3:def 3;

        y <= (a % ) by A8, YELLOW_0: 22;

        then

         A13: ( % y) [= a by A12, LATTICE3: 7;

        y = ( % y) by LATTICE3:def 4;

        then ( % y) in X by A6, A13, A3, A11;

        then ( % y) [= ( *' a) by A5, LATTICE3:def 17;

        then

         A14: (( *' a) % ) >= y by A12, LATTICE3: 7;

        x = ( % x) by LATTICE3:def 4;

        then ( % x) in X by A6, A9, A3, A10;

        then ( % x) [= ( *' a) by A5, LATTICE3:def 17;

        then (( *' a) % ) >= x by A7, LATTICE3: 7;

        then (( *' a) % ) >= (a % ) by A8, A14, YELLOW_0: 22;

        hence contradiction by A1, A2, A4, ORDERS_2: 2;

      end;

      hence thesis by WAYBEL_6:def 3;

    end;

    theorem :: LATTICE6:19

    

     Th19: for L be complete co-noetherian Lattice holds for a be Element of L st a <> ( Bottom L) holds a is completely-join-irreducible iff (a % ) is join-irreducible

    proof

      let L be complete co-noetherian Lattice;

      let a be Element of L;

      assume a <> ( Bottom L);

      then

      consider b be Element of L such that

       A1: b is-lower-neighbour-of a by Th8;

      

       A2: a <> b by A1;

      now

        assume

         A3: (a % ) is join-irreducible;

        for d be Element of L holds d is-lower-neighbour-of a implies d = b

        proof

          let d be Element of L;

          

           A4: (a % ) = a by LATTICE3:def 3;

          

           A5: (d % ) = d & (b % ) = b by LATTICE3:def 3;

          assume

           A6: d is-lower-neighbour-of a;

          then

           A7: a <> d;

          assume d <> b;

          then a = (d "\/" b) by A1, A6, Th2;

          then (a % ) = ((d % ) "\/" (b % )) by A4, Lm8;

          hence thesis by A2, A3, A7, A4, A5, WAYBEL_6:def 3;

        end;

        hence a is completely-join-irreducible by A1, Th15;

      end;

      hence thesis by Th18;

    end;

    theorem :: LATTICE6:20

    for L be finite Lattice holds for a be Element of L st a <> ( Bottom L) & a <> ( Top L) holds (a is completely-meet-irreducible iff (a % ) is meet-irreducible) & (a is completely-join-irreducible iff (a % ) is join-irreducible) by Th17, Th19;

    definition

      let L be Lattice;

      let a be Element of L;

      :: LATTICE6:def10

      attr a is atomic means a is-upper-neighbour-of ( Bottom L);

      :: LATTICE6:def11

      attr a is co-atomic means a is-lower-neighbour-of ( Top L);

    end

    theorem :: LATTICE6:21

    for L be complete Lattice holds for a be Element of L st a is atomic holds a is completely-join-irreducible

    proof

      let L be complete Lattice;

      let a be Element of L;

      set X = { x where x be Element of L : x [= a & x <> a };

      assume a is atomic;

      then

       A1: a is-upper-neighbour-of ( Bottom L);

      then

       A2: a <> ( Bottom L);

      

       A3: for x be object holds x in X implies x in {( Bottom L)}

      proof

        let x be object;

        assume x in X;

        then

         A4: ex x9 be Element of L st x9 = x & x9 [= a & x9 <> a;

        then

        reconsider x as Element of L;

        ( Bottom L) [= x by LATTICES: 16;

        then x = ( Bottom L) by A1, A4;

        hence thesis by TARSKI:def 1;

      end;

      

       A5: ( Bottom L) [= a by A1;

      

       A6: for x be object holds x in {( Bottom L)} implies x in X

      proof

        let x be object;

        assume x in {( Bottom L)};

        then x = ( Bottom L) by TARSKI:def 1;

        hence thesis by A2, A5;

      end;

      ( Bottom L) = ( "\/" ( {( Bottom L)},L)) by LATTICE3: 42

      .= ( *' a) by A3, A6, TARSKI: 2;

      hence thesis by A2;

    end;

    theorem :: LATTICE6:22

    for L be complete Lattice holds for a be Element of L st a is co-atomic holds a is completely-meet-irreducible

    proof

      let L be complete Lattice;

      let a be Element of L;

      set X = { x where x be Element of L : a [= x & x <> a };

      assume a is co-atomic;

      then

       A1: a is-lower-neighbour-of ( Top L);

      then

       A2: a <> ( Top L);

      

       A3: for x be object holds x in X implies x in {( Top L)}

      proof

        let x be object;

        assume x in X;

        then

         A4: ex x9 be Element of L st x9 = x & a [= x9 & x9 <> a;

        then

        reconsider x as Element of L;

        x [= ( Top L) by LATTICES: 19;

        then x = ( Top L) by A1, A4;

        hence thesis by TARSKI:def 1;

      end;

      

       A5: a [= ( Top L) by A1;

      

       A6: for x be object holds x in {( Top L)} implies x in X

      proof

        let x be object;

        assume x in {( Top L)};

        then x = ( Top L) by TARSKI:def 1;

        hence thesis by A2, A5;

      end;

      ( Top L) = ( "/\" ( {( Top L)},L)) by LATTICE3: 42

      .= (a *' ) by A3, A6, TARSKI: 2;

      hence thesis by A2;

    end;

    definition

      let L be Lattice;

      :: LATTICE6:def12

      attr L is atomic means for a be Element of L holds ex X be Subset of L st (for x be Element of L st x in X holds x is atomic) & a = ( "\/" (X,L));

    end

    registration

      cluster strict1 -element for Lattice;

      existence

      proof

        set X = { {} };

        set XJ = the BinOp of X;

        reconsider L = LattStr (# X, XJ, XJ #) as non empty LattStr;

        

         A1: L is trivial;

        then

         A2: (for a,b be Element of L holds ((a "/\" b) "\/" b) = b) & for a,b be Element of L holds (a "/\" b) = (b "/\" a) by STRUCT_0:def 10;

        

         A3: (for a,b,c be Element of L holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)) & for a,b be Element of L holds (a "/\" (a "\/" b)) = a by A1, STRUCT_0:def 10;

        (for a,b be Element of L holds (a "\/" b) = (b "\/" a)) & for a,b,c be Element of L holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c) by A1, STRUCT_0:def 10;

        then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A2, A3, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

        then

        reconsider L as Lattice;

        take L;

        thus thesis by STRUCT_0:def 19;

      end;

    end

    registration

      cluster atomic complete for Lattice;

      existence

      proof

        set L = the strict1 -element Lattice;

        consider x be object such that

         A1: the carrier of L = {x} by ZFMISC_1: 131;

        reconsider x as Element of L by A1, TARSKI:def 1;

        reconsider L as complete Lattice;

        for a be Element of L holds ex X be Subset of L st (for u be Element of L st u in X holds u is atomic) & a = ( "\/" (X,L))

        proof

          let a be Element of L;

          for u be object holds u in {} implies u in the carrier of L;

          then

           A2: (for u be Element of L st u in {} holds u is atomic) & {} is Subset of L by TARSKI:def 3;

          a = x & x = ( "\/" ( {} ,L)) by A1, TARSKI:def 1;

          hence thesis by A2;

        end;

        then L is atomic;

        hence thesis;

      end;

    end

    definition

      let L be complete Lattice;

      let D be Subset of L;

      :: LATTICE6:def13

      attr D is supremum-dense means for a be Element of L holds ex D9 be Subset of D st a = ( "\/" (D9,L));

      :: LATTICE6:def14

      attr D is infimum-dense means for a be Element of L holds ex D9 be Subset of D st a = ( "/\" (D9,L));

    end

    theorem :: LATTICE6:23

    

     Th23: for L be complete Lattice holds for D be Subset of L holds D is supremum-dense iff for a be Element of L holds a = ( "\/" ({ d where d be Element of L : d in D & d [= a },L))

    proof

      let L be complete Lattice;

      let D be Subset of L;

       A1:

      now

        assume

         A2: D is supremum-dense;

        thus for a be Element of L holds a = ( "\/" ({ d where d be Element of L : d in D & d [= a },L))

        proof

          let a be Element of L;

          set X = { d where d be Element of L : d in D & d [= a };

          consider D9 be Subset of D such that

           A3: a = ( "\/" (D9,L)) by A2;

          for x be object holds x in D9 implies x in X

          proof

            let x be object;

            assume

             A4: x in D9;

            then x in D;

            then

            reconsider x as Element of L;

            D9 is_less_than a by A3, LATTICE3:def 21;

            then x [= a by A4, LATTICE3:def 17;

            hence thesis by A4;

          end;

          then D9 c= X;

          then

           A5: a [= ( "\/" (X,L)) by A3, LATTICE3: 45;

          for q be Element of L st q in X holds q [= a

          proof

            let q be Element of L;

            assume q in X;

            then ex q9 be Element of L st q9 = q & q9 in D & q9 [= a;

            hence thesis;

          end;

          then X is_less_than a by LATTICE3:def 17;

          then ( "\/" (X,L)) [= a by LATTICE3:def 21;

          hence thesis by A5, LATTICES: 8;

        end;

      end;

      now

        assume

         A6: for a be Element of L holds a = ( "\/" ({ d where d be Element of L : d in D & d [= a },L));

        for a be Element of L holds ex D9 be Subset of D st a = ( "\/" (D9,L))

        proof

          let a be Element of L;

          set X = { d where d be Element of L : d in D & d [= a };

          for x be object holds x in X implies x in D

          proof

            let x be object;

            assume x in X;

            then ex x9 be Element of L st x9 = x & x9 in D & x9 [= a;

            hence thesis;

          end;

          then

           A7: X is Subset of D by TARSKI:def 3;

          a = ( "\/" (X,L)) by A6;

          hence thesis by A7;

        end;

        hence D is supremum-dense;

      end;

      hence thesis by A1;

    end;

    theorem :: LATTICE6:24

    

     Th24: for L be complete Lattice holds for D be Subset of L holds D is infimum-dense iff for a be Element of L holds a = ( "/\" ({ d where d be Element of L : d in D & a [= d },L))

    proof

      let L be complete Lattice;

      let D be Subset of L;

       A1:

      now

        assume

         A2: D is infimum-dense;

        thus for a be Element of L holds a = ( "/\" ({ d where d be Element of L : d in D & a [= d },L))

        proof

          let a be Element of L;

          set X = { d where d be Element of L : d in D & a [= d };

          consider D9 be Subset of D such that

           A3: a = ( "/\" (D9,L)) by A2;

          for x be object holds x in D9 implies x in X

          proof

            let x be object;

            assume

             A4: x in D9;

            then x in D;

            then

            reconsider x as Element of L;

            a is_less_than D9 by A3, LATTICE3: 34;

            then a [= x by A4, LATTICE3:def 16;

            hence thesis by A4;

          end;

          then D9 c= X;

          then

           A5: ( "/\" (X,L)) [= a by A3, LATTICE3: 45;

          for q be Element of L st q in X holds a [= q

          proof

            let q be Element of L;

            assume q in X;

            then ex q9 be Element of L st q9 = q & q9 in D & a [= q9;

            hence thesis;

          end;

          then a is_less_than X by LATTICE3:def 16;

          then a [= ( "/\" (X,L)) by LATTICE3: 39;

          hence thesis by A5, LATTICES: 8;

        end;

      end;

      now

        assume

         A6: for a be Element of L holds a = ( "/\" ({ d where d be Element of L : d in D & a [= d },L));

        for a be Element of L holds ex D9 be Subset of D st a = ( "/\" (D9,L))

        proof

          let a be Element of L;

          set X = { d where d be Element of L : d in D & a [= d };

          for x be object holds x in X implies x in D

          proof

            let x be object;

            assume x in X;

            then ex x9 be Element of L st x9 = x & x9 in D & a [= x9;

            hence thesis;

          end;

          then

           A7: X is Subset of D by TARSKI:def 3;

          a = ( "/\" (X,L)) by A6;

          hence thesis by A7;

        end;

        hence D is infimum-dense;

      end;

      hence thesis by A1;

    end;

    theorem :: LATTICE6:25

    for L be complete Lattice holds for D be Subset of L holds D is infimum-dense iff (D % ) is order-generating

    proof

      let L be complete Lattice;

      let D be Subset of L;

       A1:

      now

        assume

         A2: (D % ) is order-generating;

        for a be Element of L holds ex D9 be Subset of D st a = ( "/\" (D9,L))

        proof

          let a be Element of L;

          consider Y be Subset of (D % ) such that

           A3: (a % ) = ( "/\" (Y,( LattPOSet L))) by A2, WAYBEL_6: 15;

          

           A4: for x be object holds x in Y implies x in the carrier of ( LattPOSet L)

          proof

            let x be object;

            assume x in Y;

            then x in (D % );

            hence thesis;

          end;

          

           A5: (a % ) is_<=_than Y by A3, YELLOW_0: 33;

          reconsider Y as Subset of ( LattPOSet L) by A4, TARSKI:def 3;

          

           A6: for b be Element of L st b is_less_than ( % Y) holds b [= a

          proof

            let b be Element of L;

            assume

             A7: b is_less_than ( % Y);

            for u be Element of ( LattPOSet L) st u in Y holds (b % ) <= u

            proof

              let u be Element of ( LattPOSet L);

              assume u in Y;

              then ( % u) in { ( % d) where d be Element of ( LattPOSet L) : d in Y };

              then

               A8: b [= ( % u) by A7, LATTICE3:def 16;

              (( % u) % ) = ( % u) by LATTICE3:def 3

              .= u by LATTICE3:def 4;

              hence thesis by A8, LATTICE3: 7;

            end;

            then (b % ) is_<=_than Y by LATTICE3:def 8;

            then (b % ) <= (a % ) by A3, YELLOW_0: 33;

            hence thesis by LATTICE3: 7;

          end;

          for x be object holds x in ( % Y) implies x in D

          proof

            let x be object;

            assume x in ( % Y);

            then

            consider x9 be Element of ( LattPOSet L) such that

             A9: x = ( % x9) and

             A10: x9 in Y;

            x9 in (D % ) by A10;

            then

            consider y be Element of L such that

             A11: x9 = (y % ) and

             A12: y in D;

            x = (y % ) by A9, A11, LATTICE3:def 4

            .= y by LATTICE3:def 3;

            hence thesis by A12;

          end;

          then

           A13: ( % Y) is Subset of D by TARSKI:def 3;

          for q be Element of L st q in ( % Y) holds a [= q

          proof

            let q be Element of L;

            assume q in ( % Y);

            then

            consider q9 be Element of ( LattPOSet L) such that

             A14: q = ( % q9) and

             A15: q9 in Y;

            

             A16: q9 = ( % q9) by LATTICE3:def 4

            .= (( % q9) % ) by LATTICE3:def 3;

            (a % ) <= q9 by A5, A15, LATTICE3:def 8;

            hence thesis by A14, A16, LATTICE3: 7;

          end;

          then a is_less_than ( % Y) by LATTICE3:def 16;

          then a = ( "/\" (( % Y),L)) by A6, LATTICE3: 34;

          hence thesis by A13;

        end;

        hence D is infimum-dense;

      end;

      now

        assume

         A17: D is infimum-dense;

        for a be Element of ( LattPOSet L) holds ex Y be Subset of (D % ) st a = ( "/\" (Y,( LattPOSet L)))

        proof

          let a be Element of ( LattPOSet L);

          consider D9 be Subset of D such that

           A18: ( % a) = ( "/\" (D9,L)) by A17;

          

           A19: for x be object holds x in D9 implies x in the carrier of L

          proof

            let x be object;

            assume x in D9;

            then x in D;

            hence thesis;

          end;

          

           A20: ( % a) is_less_than D9 by A18, LATTICE3: 34;

          reconsider D9 as Subset of L by A19, TARSKI:def 3;

          

           A21: for b be Element of ( LattPOSet L) st (D9 % ) is_>=_than b holds b <= a

          proof

            let b be Element of ( LattPOSet L);

            

             A22: b = ( % b) by LATTICE3:def 4

            .= (( % b) % ) by LATTICE3:def 3;

            assume

             A23: (D9 % ) is_>=_than b;

            for u be Element of L st u in D9 holds ( % b) [= u

            proof

              let u be Element of L;

              assume u in D9;

              then (u % ) in { (d % ) where d be Element of L : d in D9 };

              then b <= (u % ) by A23, LATTICE3:def 8;

              hence thesis by A22, LATTICE3: 7;

            end;

            then ( % b) is_less_than D9 by LATTICE3:def 16;

            then

             A24: ( % b) [= ( % a) by A18, LATTICE3: 34;

            a = ( % a) by LATTICE3:def 4

            .= (( % a) % ) by LATTICE3:def 3;

            hence thesis by A22, A24, LATTICE3: 7;

          end;

          for x be object holds x in (D9 % ) implies x in (D % )

          proof

            let x be object;

            assume x in (D9 % );

            then ex x9 be Element of L st x = (x9 % ) & x9 in D9;

            hence thesis;

          end;

          then

           A25: (D9 % ) is Subset of (D % ) by TARSKI:def 3;

          for u be Element of ( LattPOSet L) st u in (D9 % ) holds a <= u

          proof

            let u be Element of ( LattPOSet L);

            

             A26: (( % a) % ) = ( % a) by LATTICE3:def 3

            .= a by LATTICE3:def 4;

            assume u in (D9 % );

            then

            consider u9 be Element of L such that

             A27: u = (u9 % ) and

             A28: u9 in D9;

            ( % a) [= u9 by A20, A28, LATTICE3:def 16;

            hence thesis by A27, A26, LATTICE3: 7;

          end;

          then (D9 % ) is_>=_than a by LATTICE3:def 8;

          then a = ( "/\" ((D9 % ),( LattPOSet L))) by A21, YELLOW_0: 33;

          hence thesis by A25;

        end;

        hence (D % ) is order-generating by WAYBEL_6: 15;

      end;

      hence thesis by A1;

    end;

    definition

      let L be complete Lattice;

      :: LATTICE6:def15

      func MIRRS (L) -> Subset of L equals { a where a be Element of L : a is completely-meet-irreducible };

      correctness

      proof

        set X = { a where a be Element of L : a is completely-meet-irreducible };

        for x be object holds x in X implies x in the carrier of L

        proof

          let x be object;

          assume x in X;

          then ex x9 be Element of L st x9 = x & x9 is completely-meet-irreducible;

          hence thesis;

        end;

        hence thesis by TARSKI:def 3;

      end;

      :: LATTICE6:def16

      func JIRRS (L) -> Subset of L equals { a where a be Element of L : a is completely-join-irreducible };

      correctness

      proof

        set X = { a where a be Element of L : a is completely-join-irreducible };

        for x be object holds x in X implies x in the carrier of L

        proof

          let x be object;

          assume x in X;

          then ex x9 be Element of L st x9 = x & x9 is completely-join-irreducible;

          hence thesis;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: LATTICE6:26

    for L be complete Lattice holds for D be Subset of L st D is supremum-dense holds ( JIRRS L) c= D

    proof

      let L be complete Lattice;

      let D be Subset of L;

      assume

       A1: D is supremum-dense;

      for x be object holds x in ( JIRRS L) implies x in D

      proof

        let x be object;

        assume x in ( JIRRS L);

        then

        consider x9 be Element of L such that

         A2: x9 = x and

         A3: x9 is completely-join-irreducible;

        assume

         A4: not x in D;

        reconsider x as Element of L by A2;

        set D9 = { d where d be Element of L : d in D & d [= x };

        set X = { d where d be Element of L : d [= x & d <> x };

        

         A5: not x in D9

        proof

          assume x in D9;

          then ex x9 be Element of L st x9 = x & x9 in D & x9 [= x;

          hence thesis by A4;

        end;

        for u be object holds u in D9 implies u in X

        proof

          let u be object;

          assume

           A6: u in D9;

          then ex u9 be Element of L st u9 = u & u9 in D & u9 [= x;

          hence thesis by A5, A6;

        end;

        then D9 c= X;

        then ( "\/" (D9,L)) [= ( "\/" (X,L)) by LATTICE3: 45;

        then

         A7: x [= ( "\/" (X,L)) by A1, Th23;

        for q be Element of L st q in X holds q [= x

        proof

          let q be Element of L;

          assume q in X;

          then ex q9 be Element of L st q9 = q & q9 [= x & q9 <> x;

          hence thesis;

        end;

        then X is_less_than x by LATTICE3:def 17;

        then

         A8: ( "\/" (X,L)) [= x by LATTICE3:def 21;

        ( *' x9) <> x9 by A3;

        hence thesis by A2, A7, A8, LATTICES: 8;

      end;

      hence thesis;

    end;

    theorem :: LATTICE6:27

    for L be complete Lattice holds for D be Subset of L st D is infimum-dense holds ( MIRRS L) c= D

    proof

      let L be complete Lattice;

      let D be Subset of L;

      assume

       A1: D is infimum-dense;

      let x be object;

      assume x in ( MIRRS L);

      then

      consider x9 be Element of L such that

       A2: x9 = x and

       A3: x9 is completely-meet-irreducible;

      assume

       A4: not x in D;

      reconsider x as Element of L by A2;

      set D9 = { d where d be Element of L : d in D & x [= d };

      set X = { d where d be Element of L : x [= d & d <> x };

      

       A5: not x in D9

      proof

        assume x in D9;

        then ex x9 be Element of L st x9 = x & x9 in D & x [= x9;

        hence thesis by A4;

      end;

      for u be object holds u in D9 implies u in X

      proof

        let u be object;

        assume

         A6: u in D9;

        then ex u9 be Element of L st u9 = u & u9 in D & x [= u9;

        hence thesis by A5, A6;

      end;

      then D9 c= X;

      then ( "/\" (X,L)) [= ( "/\" (D9,L)) by LATTICE3: 45;

      then

       A7: ( "/\" (X,L)) [= x by A1, Th24;

      for q be Element of L st q in X holds x [= q

      proof

        let q be Element of L;

        assume q in X;

        then ex q9 be Element of L st q9 = q & x [= q9 & q9 <> x;

        hence thesis;

      end;

      then x is_less_than X by LATTICE3:def 16;

      then

       A8: x [= ( "/\" (X,L)) by LATTICE3: 39;

      (x9 *' ) <> x9 by A3;

      hence thesis by A2, A7, A8, LATTICES: 8;

    end;

    

     Lm9: for L be co-noetherian complete Lattice holds ( MIRRS L) is infimum-dense

    proof

      let L be co-noetherian complete Lattice;

      defpred P[ Element of (( LattPOSet L) ~ )] means ex D9 be Subset of ( MIRRS L) st $1 = (( "/\" (D9,L)) % );

      

       A1: for x be Element of (( LattPOSet L) ~ ) st for y be Element of (( LattPOSet L) ~ ) st y <> x & [y, x] in the InternalRel of (( LattPOSet L) ~ ) holds P[y] holds P[x]

      proof

        let x be Element of (( LattPOSet L) ~ );

        set X = { d where d be Element of L : ( % ( ~ x)) [= d & d <> ( % ( ~ x)) };

        

         A2: for u be Element of L st u in X holds ((u % ) ~ ) <> x & [((u % ) ~ ), x] in the InternalRel of (( LattPOSet L) ~ )

        proof

          let u be Element of L;

          

           A3: ((( % ( ~ x)) % ) ~ ) = (( % ( ~ x)) % ) by LATTICE3:def 6

          .= ( % ( ~ x)) by LATTICE3:def 3

          .= ( ~ x) by LATTICE3:def 4

          .= x by LATTICE3:def 7;

          assume u in X;

          then

           A4: ex u9 be Element of L st u9 = u & ( % ( ~ x)) [= u9 & ( % ( ~ x)) <> u9;

          then (( % ( ~ x)) % ) <= (u % ) by LATTICE3: 7;

          then

           A5: ((u % ) ~ ) <= x by A3, LATTICE3: 9;

          

           A6: ((u % ) ~ ) = (u % ) by LATTICE3:def 6

          .= u by LATTICE3:def 3;

          ( % ( ~ x)) = ( ~ x) by LATTICE3:def 4

          .= x by LATTICE3:def 7;

          hence thesis by A4, A5, A6, ORDERS_2:def 5;

        end;

        assume

         A7: for y be Element of (( LattPOSet L) ~ ) st y <> x & [y, x] in the InternalRel of (( LattPOSet L) ~ ) holds P[y];

        

         A8: for u be Element of L st u in X holds P[((u % ) ~ )]

        proof

          let u be Element of L;

          assume u in X;

          then ((u % ) ~ ) <> x & [((u % ) ~ ), x] in the InternalRel of (( LattPOSet L) ~ ) by A2;

          hence thesis by A7;

        end;

        per cases ;

          suppose ( % ( ~ x)) is completely-meet-irreducible;

          then ( % ( ~ x)) in { a where a be Element of L : a is completely-meet-irreducible };

          then for y be object holds y in {( % ( ~ x))} implies y in ( MIRRS L) by TARSKI:def 1;

          then

           A9: {( % ( ~ x))} is Subset of ( MIRRS L) by TARSKI:def 3;

          (( "/\" ( {( % ( ~ x))},L)) % ) = ( "/\" ( {( % ( ~ x))},L)) by LATTICE3:def 3

          .= ( % ( ~ x)) by LATTICE3: 42

          .= ( ~ x) by LATTICE3:def 4

          .= x by LATTICE3:def 7;

          hence thesis by A9;

        end;

          suppose

           A10: not ( % ( ~ x)) is completely-meet-irreducible;

          set G = { H where H be Subset of ( MIRRS L) : ex u be Element of ( LattPOSet L) st ( % u) in X & ( % u) = ( "/\" (H,L)) };

          set D9 = ( union G);

          

           A11: (( % ( ~ x)) *' ) = ( % ( ~ x)) by A10;

          

           A12: for r be Element of L st r is_less_than D9 holds r [= ( % ( ~ x))

          proof

            let r be Element of L;

            assume

             A13: r is_less_than D9;

            for q be Element of L st q in X holds r [= q

            proof

              let q be Element of L;

              assume

               A14: q in X;

              then

              consider D be Subset of ( MIRRS L) such that

               A15: ((q % ) ~ ) = (( "/\" (D,L)) % ) by A8;

              

               A16: (q % ) = q by LATTICE3:def 3;

              for v be object holds v in D implies v in D9

              proof

                let v be object;

                ((q % ) ~ ) = (q % ) by LATTICE3:def 6

                .= ( % (q % )) by LATTICE3:def 4;

                then

                 A17: ( % (q % )) = ( "/\" (D,L)) by A15, LATTICE3:def 3;

                ( % (q % )) in X by A14, A16, LATTICE3:def 4;

                then

                 A18: D in G by A17;

                assume v in D;

                hence thesis by A18, TARSKI:def 4;

              end;

              then D c= D9;

              then for p be Element of L st p in D holds r [= p by A13, LATTICE3:def 16;

              then

               A19: r is_less_than D by LATTICE3:def 16;

              q = ((q % ) ~ ) by A16, LATTICE3:def 6

              .= ( "/\" (D,L)) by A15, LATTICE3:def 3;

              hence thesis by A19, LATTICE3: 34;

            end;

            then r is_less_than X by LATTICE3:def 16;

            hence thesis by A11, LATTICE3: 34;

          end;

          for v be object holds v in D9 implies v in ( MIRRS L)

          proof

            let v be object;

            assume v in D9;

            then

            consider v9 be set such that

             A20: v in v9 and

             A21: v9 in G by TARSKI:def 4;

            ex H be Subset of ( MIRRS L) st H = v9 & ex u be Element of ( LattPOSet L) st ( % u) in X & ( % u) = ( "/\" (H,L)) by A21;

            hence thesis by A20;

          end;

          then

           A22: D9 is Subset of ( MIRRS L) by TARSKI:def 3;

          

           A23: ( % ( ~ x)) = ( ~ x) by LATTICE3:def 4

          .= x by LATTICE3:def 7;

          

           A24: (( "/\" (D9,L)) % ) = ( "/\" (D9,L)) by LATTICE3:def 3;

          for q be Element of L st q in D9 holds ( % ( ~ x)) [= q

          proof

            let q be Element of L;

            assume q in D9;

            then

            consider h be set such that

             A25: q in h and

             A26: h in G by TARSKI:def 4;

            ex h9 be Subset of ( MIRRS L) st h9 = h & ex u be Element of ( LattPOSet L) st ( % u) in X & ( % u) = ( "/\" (h9,L)) by A26;

            then

            consider u be Element of ( LattPOSet L) such that

             A27: ( % u) in X and

             A28: ( % u) = ( "/\" (h,L));

            ( % u) is_less_than h by A28, LATTICE3: 34;

            then

             A29: ( % u) [= q by A25, LATTICE3:def 16;

            ( % ( ~ x)) is_less_than X by A11, LATTICE3: 34;

            then ( % ( ~ x)) [= ( % u) by A27, LATTICE3:def 16;

            hence thesis by A29, LATTICES: 7;

          end;

          then ( % ( ~ x)) is_less_than D9 by LATTICE3:def 16;

          then ( % ( ~ x)) = ( "/\" (D9,L)) by A12, LATTICE3: 34;

          hence thesis by A22, A23, A24;

        end;

      end;

      

       A30: (( LattPOSet L) ~ ) is well_founded by Def4;

      

       A31: for x be Element of (( LattPOSet L) ~ ) holds P[x] from WELLFND1:sch 3( A1, A30);

      for a be Element of L holds ex D9 be Subset of ( MIRRS L) st a = ( "/\" (D9,L))

      proof

        let a be Element of L;

        (( LattPOSet L) ~ ) = RelStr (# the carrier of ( LattPOSet L), (the InternalRel of ( LattPOSet L) ~ ) #) by LATTICE3:def 5;

        then

        reconsider a9 = (a % ) as Element of (( LattPOSet L) ~ );

        (ex D9 be Subset of ( MIRRS L) st a9 = (( "/\" (D9,L)) % )) & (a % ) = a by A31, LATTICE3:def 3;

        hence thesis by LATTICE3:def 3;

      end;

      hence thesis;

    end;

    registration

      let L be co-noetherian complete Lattice;

      cluster ( MIRRS L) -> infimum-dense;

      coherence by Lm9;

    end

    

     Lm10: for L be noetherian complete Lattice holds ( JIRRS L) is supremum-dense

    proof

      let L be noetherian complete Lattice;

      defpred P[ Element of ( LattPOSet L)] means ex D9 be Subset of ( JIRRS L) st ( % $1) = ( "\/" (D9,L));

      

       A1: for x be Element of ( LattPOSet L) st for y be Element of ( LattPOSet L) st y <> x & [y, x] in the InternalRel of ( LattPOSet L) holds P[y] holds P[x]

      proof

        let x be Element of ( LattPOSet L);

        set X = { d where d be Element of L : d [= ( % x) & d <> ( % x) };

        

         A2: for u be Element of L st u in X holds (u % ) <> x & [(u % ), x] in the InternalRel of ( LattPOSet L)

        proof

          let u be Element of L;

          assume u in X;

          then

           A3: ex u9 be Element of L st u9 = u & u9 [= ( % x) & ( % x) <> u9;

          

           A4: ( % x) = x by LATTICE3:def 4;

          then (( % x) % ) = x by LATTICE3:def 3;

          then (u % ) <= x by A3, LATTICE3: 7;

          hence thesis by A3, A4, LATTICE3:def 3, ORDERS_2:def 5;

        end;

        assume

         A5: for y be Element of ( LattPOSet L) st y <> x & [y, x] in the InternalRel of ( LattPOSet L) holds P[y];

        

         A6: for u be Element of L st u in X holds P[(u % )]

        proof

          let u be Element of L;

          assume u in X;

          then (u % ) <> x & [(u % ), x] in the InternalRel of ( LattPOSet L) by A2;

          hence thesis by A5;

        end;

        per cases ;

          suppose ( % x) is completely-join-irreducible;

          then ( % x) in { a where a be Element of L : a is completely-join-irreducible };

          then for y be object holds y in {( % x)} implies y in ( JIRRS L) by TARSKI:def 1;

          then

           A7: {( % x)} is Subset of ( JIRRS L) by TARSKI:def 3;

          ( "\/" ( {( % x)},L)) = ( % x) by LATTICE3: 42;

          hence thesis by A7;

        end;

          suppose

           A8: not ( % x) is completely-join-irreducible;

          set G = { H where H be Subset of ( JIRRS L) : ex u be Element of ( LattPOSet L) st ( % u) in X & ( % u) = ( "\/" (H,L)) };

          set D9 = ( union G);

          

           A9: ( *' ( % x)) = ( % x) by A8;

          

           A10: for r be Element of L st D9 is_less_than r holds ( % x) [= r

          proof

            let r be Element of L;

            assume

             A11: D9 is_less_than r;

            for q be Element of L st q in X holds q [= r

            proof

              let q be Element of L;

              assume

               A12: q in X;

              then

              consider D be Subset of ( JIRRS L) such that

               A13: ( % (q % )) = ( "\/" (D,L)) by A6;

              (q % ) = q by LATTICE3:def 3;

              then

               A14: q = ( "\/" (D,L)) by A13, LATTICE3:def 4;

              for v be object holds v in D implies v in D9

              proof

                let v be object;

                assume

                 A15: v in D;

                D in G by A12, A13, A14;

                hence thesis by A15, TARSKI:def 4;

              end;

              then D c= D9;

              then for p be Element of L st p in D holds p [= r by A11, LATTICE3:def 17;

              then D is_less_than r by LATTICE3:def 17;

              hence thesis by A14, LATTICE3:def 21;

            end;

            then X is_less_than r by LATTICE3:def 17;

            hence thesis by A9, LATTICE3:def 21;

          end;

          for v be object holds v in D9 implies v in ( JIRRS L)

          proof

            let v be object;

            assume v in D9;

            then

            consider v9 be set such that

             A16: v in v9 and

             A17: v9 in G by TARSKI:def 4;

            ex H be Subset of ( JIRRS L) st H = v9 & ex u be Element of ( LattPOSet L) st ( % u) in X & ( % u) = ( "\/" (H,L)) by A17;

            hence thesis by A16;

          end;

          then

           A18: D9 is Subset of ( JIRRS L) by TARSKI:def 3;

          for q be Element of L st q in D9 holds q [= ( % x)

          proof

            let q be Element of L;

            assume q in D9;

            then

            consider h be set such that

             A19: q in h and

             A20: h in G by TARSKI:def 4;

            ex h9 be Subset of ( JIRRS L) st h9 = h & ex u be Element of ( LattPOSet L) st ( % u) in X & ( % u) = ( "\/" (h9,L)) by A20;

            then

            consider u be Element of ( LattPOSet L) such that

             A21: ( % u) in X and

             A22: ( % u) = ( "\/" (h,L));

            h is_less_than ( % u) by A22, LATTICE3:def 21;

            then

             A23: q [= ( % u) by A19, LATTICE3:def 17;

            X is_less_than ( % x) by A9, LATTICE3:def 21;

            then ( % u) [= ( % x) by A21, LATTICE3:def 17;

            hence thesis by A23, LATTICES: 7;

          end;

          then D9 is_less_than ( % x) by LATTICE3:def 17;

          then ( % x) = ( "\/" (D9,L)) by A10, LATTICE3:def 21;

          hence thesis by A18;

        end;

      end;

      

       A24: ( LattPOSet L) is well_founded by Def3;

      

       A25: for x be Element of ( LattPOSet L) holds P[x] from WELLFND1:sch 3( A1, A24);

      for a be Element of L holds ex D9 be Subset of ( JIRRS L) st a = ( "\/" (D9,L))

      proof

        let a be Element of L;

        ( % (a % )) = (a % ) by LATTICE3:def 4

        .= a by LATTICE3:def 3;

        hence thesis by A25;

      end;

      hence thesis;

    end;

    registration

      let L be noetherian complete Lattice;

      cluster ( JIRRS L) -> supremum-dense;

      coherence by Lm10;

    end