filter_0.miz

    begin

    reserve L for Lattice,

p,p1,q,q1,r,r1 for Element of L;

    reserve x,y,z,X,Y,Z,X1,X2 for set;

    theorem :: FILTER_0:1



     Th1: for L be join-associative join-commutative meet-commutative join-absorbing meet-absorbing non empty LattStr, p,q,r be Element of L st p [= q holds (r "\/" p) [= (r "\/" q)

    proof

      let L be join-associative join-commutative meet-commutative join-absorbing meet-absorbing non empty LattStr, p,q,r be Element of L;

      assume

       A1: (p "\/" q) = q;



      thus ((r "\/" p) "\/" (r "\/" q)) = ((r "\/" (r "\/" p)) "\/" q) by LATTICES:def 5

      .= (((r "\/" r) "\/" p) "\/" q) by LATTICES:def 5

      .= ((r "\/" p) "\/" q)

      .= (r "\/" q) by A1, LATTICES:def 5;

    end;

    theorem :: FILTER_0:2

    p [= r implies (p "/\" q) [= r

    proof

      assume p [= r;

      then

       A1: (p "/\" q) [= (r "/\" q) by LATTICES: 9;

      (r "/\" q) [= r by LATTICES: 6;

      hence thesis by A1, LATTICES: 7;

    end;

    theorem :: FILTER_0:3

    p [= r implies p [= (q "\/" r)

    proof

      assume p [= r;

      then

       A1: (p "\/" q) [= (r "\/" q) by Th1;

      p [= (p "\/" q) by LATTICES: 5;

      hence thesis by A1, LATTICES: 7;

    end;

    theorem :: FILTER_0:4



     Th4: for L be join-absorbing join-commutative join-associative non empty LattStr, a,b,c,d be Element of L st a [= b & c [= d holds (a "\/" c) [= (b "\/" d)

    proof

      let L be join-absorbing join-commutative join-associative non empty LattStr, a,b,c,d be Element of L;

      assume a [= b;

      then

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

      assume c [= d;



      then (b "\/" d) = ((a "\/" b) "\/" (c "\/" d)) by A1

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

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

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

      hence thesis;

    end;

    theorem :: FILTER_0:5



     Th5: for L be meet-absorbing meet-commutative join-absorbing meet-associative non empty LattStr, a,b,c,d be Element of L st a [= b & c [= d holds (a "/\" c) [= (b "/\" d)

    proof

      let L be meet-absorbing meet-commutative meet-associative join-absorbing non empty LattStr, a,b,c,d be Element of L;

      assume a [= b;

      then

       A1: (a "/\" b) = a by LATTICES: 4;

      assume c [= d;



      then (a "/\" c) = ((a "/\" b) "/\" (c "/\" d)) by A1, LATTICES: 4

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

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

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

      hence thesis by LATTICES: 4;

    end;

    theorem :: FILTER_0:6



     Th6: for L be join-absorbing join-commutative join-associative meet-absorbing meet-commutative non empty LattStr, a,b,c be Element of L st a [= c & b [= c holds (a "\/" b) [= c

    proof

      let L be join-absorbing join-commutative join-associative meet-absorbing meet-commutative non empty LattStr, a,b,c be Element of L;

      (c "\/" c) = c;

      hence thesis by Th4;

    end;

    theorem :: FILTER_0:7



     Th7: for L be meet-absorbing meet-commutative join-absorbing meet-associative non empty LattStr, a,b,c be Element of L st a [= b & a [= c holds a [= (b "/\" c)

    proof

      let L be meet-absorbing meet-commutative join-absorbing meet-associative non empty LattStr, a,b,c be Element of L;

      (a "/\" a) = a;

      hence thesis by Th5;

    end;

    definition

      let L;

      mode Filter of L is non empty meet-closed final Subset of L;

    end

    theorem :: FILTER_0:8



     Th8: for S be non empty Subset of L holds S is Filter of L iff for p,q be Element of L holds p in S & q in S iff (p "/\" q) in S

    proof

      let S be non empty Subset of L;

      thus S is Filter of L implies for p,q be Element of L holds p in S & q in S iff (p "/\" q) in S by LATTICES: 6, LATTICES:def 23, LATTICES:def 24;

      assume

       A1: for p,q be Element of L holds p in S & q in S iff (p "/\" q) in S;

      S is final

      proof

        let p,q be Element of L such that

         A2: p [= q and

         A3: p in S;

        (p "/\" q) = p by A2, LATTICES: 4;

        hence q in S by A1, A3;

      end;

      hence thesis by A1, LATTICES:def 24;

    end;

    theorem :: FILTER_0:9



     Th9: for D be non empty Subset of L holds D is Filter of L iff (for p, q st p in D & q in D holds (p "/\" q) in D) & for p, q st p in D & p [= q holds q in D

    proof

      let D be non empty Subset of L;

      thus D is Filter of L implies (for p, q st p in D & q in D holds (p "/\" q) in D) & for p, q st p in D & p [= q holds q in D by LATTICES:def 23, LATTICES:def 24;

      assume

       A1: (for p, q st p in D & q in D holds (p "/\" q) in D) & for p, q st p in D & p [= q holds q in D;

      then for p, q st p [= q & p in D holds q in D;

      hence thesis by A1, LATTICES:def 23, LATTICES:def 24;

    end;

    reserve H,F for Filter of L;

    theorem :: FILTER_0:10



     Th10: p in H implies (p "\/" q) in H & (q "\/" p) in H

    proof

      p [= (p "\/" q) by LATTICES: 5;

      hence thesis by Th9;

    end;

    theorem :: FILTER_0:11



     Th11: L is 1_Lattice implies ( Top L) in H

    proof

      assume L is 1_Lattice;

      then

      reconsider L as 1_Lattice;

      consider p be Element of L such that

       A1: p in H by SUBSET_1: 4;

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

      hence thesis by A1, Th9;

    end;

    theorem :: FILTER_0:12

    L is 1_Lattice implies {( Top L)} is Filter of L

    proof

      assume L is 1_Lattice;

      then

      reconsider K = L as 1_Lattice;

      now

        let p,q be Element of K;



         A1: p in {( Top K)} iff p = ( Top K) by TARSKI:def 1;

        hence p in {( Top K)} & q in {( Top K)} implies (p "/\" q) in {( Top K)};

        assume (p "/\" q) in {( Top K)};

        then

         A2: (p "/\" q) = ( Top K) by TARSKI:def 1;

        (p "/\" q) [= p & (q "/\" p) [= q by LATTICES: 6;

        hence p in {( Top K)} & q in {( Top K)} by A1, A2;

      end;

      hence thesis by Th8;

    end;

    theorem :: FILTER_0:13

     {p} is Filter of L implies L is upper-bounded

    proof

      assume {p} is Filter of L;

      then

      reconsider F = {p} as Filter of L;

      take p;

      let q;

      p in F by TARSKI:def 1;

      then (p "\/" q) in F by Th10;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FILTER_0:14



     Th14: the carrier of L is Filter of L

    proof

      the carrier of L = ( [#] L);

      hence thesis;

    end;

    definition

      let L;

      :: FILTER_0:def1

      func <.L.) -> Filter of L equals the carrier of L;

      coherence by Th14;

    end

    definition

      let L, p;

      :: FILTER_0:def2

      func <.p.) -> Filter of L equals { q : p [= q };

      coherence

      proof

        set D = { q : p [= q };

        p in D;

        then

        reconsider F = D as non empty set;

        F c= the carrier of L

        proof

          let x be object;

          assume x in F;

          then ex q st x = q & p [= q;

          hence thesis;

        end;

        then

        reconsider F as non empty Subset of L;

         A1:

        now

          let r, q;

          assume r in F;

          then ex r1 st r = r1 & p [= r1;

          then

           A2: (p "/\" p) [= (r "/\" p) by LATTICES: 9;

          assume q in F;

          then ex q1 st q = q1 & p [= q1;

          then

           A3: (p "/\" r) [= (q "/\" r) by LATTICES: 9;

          p [= (r "/\" q) by A3, A2, LATTICES: 7;

          hence (r "/\" q) in F;

        end;

        now

          let r, q;

          assume r in F;

          then

           A4: ex r1 st r = r1 & p [= r1;

          assume r [= q;

          then p [= q by A4, LATTICES: 7;

          hence q in F;

        end;

        hence thesis by A1, Th9;

      end;

    end

    theorem :: FILTER_0:15



     Th15: q in <.p.) iff p [= q

    proof

      q in <.p.) iff ex r st q = r & p [= r;

      hence thesis;

    end;

    theorem :: FILTER_0:16



     Th16: p in <.p.) & (p "\/" q) in <.p.) & (q "\/" p) in <.p.)

    proof

      p [= (p "\/" q) by LATTICES: 5;

      hence thesis;

    end;

    theorem :: FILTER_0:17



     Th17: L is 0_Lattice implies <.L.) = <.( Bottom L).)

    proof

      assume L is 0_Lattice;

      then

      reconsider L9 = L as 0_Lattice;

      thus <.L.) c= <.( Bottom L).)

      proof

        let x be object;

        assume x in <.L.);

        then

        reconsider x as Element of L9;

        ( Bottom L) in <.( Bottom L).) & (x "/\" ( Bottom L9)) = ( Bottom L9);

        hence thesis by Th8;

      end;

      thus thesis;

    end;

    definition

      let L, F;

      :: FILTER_0:def3

      attr F is being_ultrafilter means F <> the carrier of L & for H st F c= H & H <> the carrier of L holds F = H;

    end

    theorem :: FILTER_0:18



     Th18: L is lower-bounded implies for F st F <> the carrier of L holds ex H st F c= H & H is being_ultrafilter

    proof

      given r such that

       A1: for p holds (r "/\" p) = r & (p "/\" r) = r;



       A2: r in H implies H = the carrier of L

      proof

        assume

         A3: r in H;

        thus H c= the carrier of L;

        let x be object;

        assume x in the carrier of L;

        then

        reconsider p = x as Element of L;

        (r "/\" p) = r by A1;

        then r [= p by LATTICES: 4;

        hence thesis by A3, Th9;

      end;

      let F such that

       A4: F <> the carrier of L;

      set X = { A where A be Subset of L : F c= A & A is Filter of L & A <> the carrier of L };



       A5: x in X implies x is Subset of L & x is Filter of L

      proof

        assume x in X;

        then ex A be Subset of L st x = A & F c= A & A is Filter of L & A <> the carrier of L;

        hence thesis;

      end;



       A6: X1 in X implies (F,X1) are_c=-comparable & X1 <> the carrier of L

      proof

        assume X1 in X;

        then ex A be Subset of L st X1 = A & F c= A & A is Filter of L & A <> the carrier of L;

        hence thesis;

      end;



       A7: for Z st Z c= X & Z is c=-linear holds ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y

      proof

        set x = the Element of F;

        let Z such that

         A8: Z c= X and

         A9: Z is c=-linear;

        take Y = ( union (Z \/ {F}));

        F in {F} by TARSKI:def 1;

        then

         A10: F in (Z \/ {F}) by XBOOLE_0:def 3;

        x in F;

        then

        reconsider V = Y as non empty set by A10, TARSKI:def 4;

        V c= the carrier of L

        proof

          let x be object;

          assume x in V;

          then

          consider X1 such that

           A11: x in X1 and

           A12: X1 in (Z \/ {F}) by TARSKI:def 4;

          X1 in Z or X1 in {F} by A12, XBOOLE_0:def 3;

          then X1 is Subset of L by A5, A8;

          hence thesis by A11;

        end;

        then

        reconsider V as non empty Subset of L;

        now

          let p, q;

          thus p in V & q in V implies (p "/\" q) in V

          proof

            assume p in V;

            then

            consider X1 such that

             A13: p in X1 and

             A14: X1 in (Z \/ {F}) by TARSKI:def 4;



             A15: X1 in Z or X1 in {F} by A14, XBOOLE_0:def 3;

            then

             A16: X1 in X & X1 in Z or X1 = F by A8, TARSKI:def 1;

            assume q in V;

            then

            consider X2 such that

             A17: q in X2 and

             A18: X2 in (Z \/ {F}) by TARSKI:def 4;



             A19: X2 in Z or X2 in {F} by A18, XBOOLE_0:def 3;

            then X2 in X & X2 in Z or X2 = F by A8, TARSKI:def 1;

            then (X1,X2) are_c=-comparable by A6, A9, A16, ORDINAL1:def 8;

            then

             A20: X1 c= X2 or X2 c= X1;



             A21: X1 is Filter of L by A5, A8, A15, TARSKI:def 1;

            X2 is Filter of L by A5, A8, A19, TARSKI:def 1;

            then (p "/\" q) in X1 or (p "/\" q) in X2 by A13, A17, A20, A21, Th9;

            hence thesis by A14, A18, TARSKI:def 4;

          end;

          assume (p "/\" q) in V;

          then

          consider X1 such that

           A22: (p "/\" q) in X1 and

           A23: X1 in (Z \/ {F}) by TARSKI:def 4;

          X1 in Z or X1 in {F} by A23, XBOOLE_0:def 3;

          then X1 is Filter of L by A5, A8, TARSKI:def 1;

          then p in X1 & q in X1 by A22, Th8;

          hence p in V & q in V by A23, TARSKI:def 4;

        end;

        then

        reconsider V as Filter of L by Th8;

        now

          assume r in V;

          then

          consider X1 such that

           A24: r in X1 and

           A25: X1 in (Z \/ {F}) by TARSKI:def 4;

          X1 in Z or X1 in {F} by A25, XBOOLE_0:def 3;

          then X1 in X or X1 = F by A8, TARSKI:def 1;

          then ex A be Subset of L st X1 = A & F c= A & A is Filter of L & A <> the carrier of L by A4;

          hence contradiction by A2, A24;

        end;

        then

         A26: V <> the carrier of L;

        F c= V by A10, TARSKI:def 4;

        hence Y in X by A26;

        let X1;

        assume X1 in Z;

        then X1 in (Z \/ {F}) by XBOOLE_0:def 3;

        hence thesis by ZFMISC_1: 74;

      end;

      F in X by A4;

      then

      consider Y such that

       A27: Y in X and

       A28: for Z st Z in X & Z <> Y holds not Y c= Z by A7, ORDERS_1: 65;

      consider H be Subset of L such that

       A29: Y = H and

       A30: F c= H and

       A31: H is Filter of L and

       A32: H <> the carrier of L by A27;

      reconsider H as Filter of L by A31;

      take H;

      thus F c= H & H <> the carrier of L by A30, A32;

      let G be Filter of L;

      assume that

       A33: H c= G and

       A34: G <> the carrier of L;

      F c= G by A30, A33;

      then G in X by A34;

      hence thesis by A28, A29, A33;

    end;

    theorem :: FILTER_0:19



     Th19: (ex r st (p "/\" r) <> p) implies <.p.) <> the carrier of L

    proof

      given r such that

       A1: (p "/\" r) <> p;

      (p "/\" r) [= p by LATTICES: 6;

      then not p [= (p "/\" r) by A1, LATTICES: 8;

      hence thesis by Th15;

    end;

    theorem :: FILTER_0:20



     Th20: L is 0_Lattice & p <> ( Bottom L) implies ex H st p in H & H is being_ultrafilter

    proof

      assume that

       A1: L is 0_Lattice and

       A2: p <> ( Bottom L);

      reconsider L9 = L as 0_Lattice by A1;

      reconsider p9 = p as Element of L9;

      (p9 "/\" ( Bottom L9)) = ( Bottom L9);

      then

      consider H such that

       A3: <.p.) c= H & H is being_ultrafilter by A2, Th18, Th19;

      take H;

      p in <.p.);

      hence thesis by A3;

    end;

    reserve D for non empty Subset of L;

    definition

      let L, D;

      :: FILTER_0:def4

      func <.D.) -> Filter of L means

      : Def4: D c= it & for F st D c= F holds it c= F;

      existence

      proof

        set x = the Element of D;

        defpred P[ set] means $1 is Filter of L & D c= $1;

        consider X such that

         A1: Z in X iff Z in ( bool the carrier of L) & P[Z] from XFAMILY:sch 1;

        reconsider x as Element of L;

         <.L.) = the carrier of L;

        then

         A2: X <> {} by A1;

        now

          let Z;

          assume Z in X;

          then D c= Z by A1;

          hence x in Z;

        end;

        then

        reconsider F = ( meet X) as non empty set by A2, SETFAM_1:def 1;



         A3: <.L.) in X by A1;

        F c= the carrier of L by A3, SETFAM_1:def 1;

        then

        reconsider F as non empty Subset of L;

        now

          let p, q;

          thus p in F & q in F implies (p "/\" q) in F

          proof

            assume

             A4: p in F & q in F;

            for Z st Z in X holds (p "/\" q) in Z

            proof

              let Z;

              assume

               A5: Z in X;

              then

              reconsider Z9 = Z as Filter of L by A1;

              p in Z9 & q in Z9 by A4, A5, SETFAM_1:def 1;

              hence thesis by Th8;

            end;

            hence thesis by A2, SETFAM_1:def 1;

          end;

          assume

           A6: (p "/\" q) in F;

          now

            let Z;

            assume

             A7: Z in X;

            then

            reconsider Z9 = Z as Filter of L by A1;

            (p "/\" q) in Z9 by A6, A7, SETFAM_1:def 1;

            hence p in Z by Th8;

          end;

          hence p in F by A2, SETFAM_1:def 1;

          now

            let Z;

            assume

             A8: Z in X;

            then

            reconsider Z9 = Z as Filter of L by A1;

            (p "/\" q) in Z9 by A6, A8, SETFAM_1:def 1;

            hence q in Z by Th8;

          end;

          hence q in F by A2, SETFAM_1:def 1;

        end;

        then

        reconsider F as Filter of L by Th8;

        take F;

        for Z st Z in X holds D c= Z by A1;

        hence D c= F by A2, SETFAM_1: 5;

        let H;

        assume D c= H;

        then H in X by A1;

        hence thesis by SETFAM_1: 3;

      end;

      uniqueness ;

    end

    theorem :: FILTER_0:21



     Th21: <.F.) = F by Def4;

    reserve D1,D2 for non empty Subset of L;

    theorem :: FILTER_0:22



     Th22: D1 c= D2 implies <.D1.) c= <.D2.)

    proof

      assume

       A1: D1 c= D2;

      D2 c= <.D2.) by Def4;

      then D1 c= <.D2.) by A1;

      hence thesis by Def4;

    end;

    theorem :: FILTER_0:23



     Th23: p in D implies <.p.) c= <.D.)

    proof

      assume

       A1: p in D;

      let x be object;



       A2: D c= <.D.) by Def4;

      assume x in <.p.);

      then ex q st x = q & p [= q;

      hence thesis by A1, A2, Th9;

    end;

    theorem :: FILTER_0:24



     Th24: D = {p} implies <.D.) = <.p.)

    proof

      assume

       A1: D = {p};

      D c= <.p.)

      proof

        let x be object;

        assume x in D;

        then x = p by A1, TARSKI:def 1;

        hence thesis;

      end;

      hence <.D.) c= <.p.) by Def4;

      p in D by A1, TARSKI:def 1;

      hence thesis by Th23;

    end;

    theorem :: FILTER_0:25



     Th25: L is 0_Lattice & ( Bottom L) in D implies <.D.) = <.L.) & <.D.) = the carrier of L

    proof

      assume that

       A1: L is 0_Lattice and

       A2: ( Bottom L) in D;



       A3: <.( Bottom L).) = <.L.) by A1, Th17;

      hence <.D.) c= <.L.) & <.L.) c= <.D.) by A2, Th23;

      thus <.D.) c= the carrier of L & the carrier of L c= <.D.) by A2, A3, Th23;

    end;

    theorem :: FILTER_0:26



     Th26: L is 0_Lattice & ( Bottom L) in F implies F = <.L.) & F = the carrier of L

    proof

      F = <.F.) by Th21;

      hence thesis by Th25;

    end;

    definition

      let L, F;

      :: FILTER_0:def5

      attr F is prime means (p "\/" q) in F iff p in F or q in F;

    end

    theorem :: FILTER_0:27



     Th27: L is B_Lattice implies for p, q holds (p "/\" ((p ` ) "\/" q)) [= q & for r st (p "/\" r) [= q holds r [= ((p ` ) "\/" q)

    proof

      assume L is B_Lattice;

      then

      reconsider S = L as B_Lattice;

      reconsider J = S as 1_Lattice;

      reconsider K = S as 0_Lattice;

      let p, q;

      set r = ((p ` ) "\/" q);

      reconsider p9 = p, q9 = q as Element of K;

      reconsider p99 = p as Element of S;



       A1: (p99 "/\" (p99 ` )) = ( Bottom L) & (( Bottom K) "\/" (p9 "/\" q9)) = (p9 "/\" q9) by LATTICES: 20;

      reconsider K = S as D_Lattice;

      reconsider p9 = p, q9 = q, r9 = r as Element of K;

      (p9 "/\" r9) = ((p9 "/\" (p9 ` )) "\/" (p9 "/\" q9)) by LATTICES:def 11;

      hence (p "/\" r) [= q by A1, LATTICES: 6;

      let r1;

      reconsider r19 = r1 as Element of K;

      reconsider pp = p, r99 = r1 as Element of J;



       A2: ((p99 ` ) "\/" p99) = ( Top L) & (( Top J) "/\" ((pp ` ) "\/" r99)) = ((pp ` ) "\/" r99) by LATTICES: 21;

      assume (p "/\" r1) [= q;

      then

       A3: ((p ` ) "\/" (p "/\" r1)) [= r by Th1;

      ((p9 ` ) "\/" (p9 "/\" r19)) = (((p9 ` ) "\/" p9) "/\" ((p9 ` ) "\/" r19)) & r1 [= (r1 "\/" (p ` )) by LATTICES: 5, LATTICES: 11;

      hence thesis by A3, A2, LATTICES: 7;

    end;

    definition

      let IT be non empty LattStr;

      :: FILTER_0:def6

      attr IT is implicative means

      : Def6: for p,q be Element of IT holds ex r be Element of IT st (p "/\" r) [= q & for r1 be Element of IT st (p "/\" r1) [= q holds r1 [= r;

    end

    registration

      cluster strict implicative for Lattice;

      existence

      proof

        set L = the strict B_Lattice;

        now

          let p,q be Element of L;

          reconsider r = ((p ` ) "\/" q) as Element of L;

          take r;

          thus (p "/\" r) [= q & for r1 be Element of L st (p "/\" r1) [= q holds r1 [= r by Th27;

        end;

        then L is implicative;

        hence thesis;

      end;

    end

    definition

      mode I_Lattice is implicative Lattice;

    end

    definition

      let L, p, q;

      assume

       A1: L is I_Lattice;

      :: FILTER_0:def7

      func p => q -> Element of L means

      : Def7: (p "/\" it ) [= q & for r st (p "/\" r) [= q holds r [= it ;

      existence by A1, Def6;

      correctness

      proof

        let r1,r2 be Element of L;

        assume (p "/\" r1) [= q & (for r st (p "/\" r) [= q holds r [= r1) & (p "/\" r2) [= q & for r st (p "/\" r) [= q holds r [= r2;

        then r1 [= r2 & r2 [= r1;

        hence thesis by LATTICES: 8;

      end;

    end

    reserve I for I_Lattice,

i,j,k for Element of I;

    registration

      cluster -> upper-bounded for I_Lattice;

      coherence

      proof

        let I;

        set i = the Element of I;

        take k = (i => i);

        let j;

        (i "/\" j) [= i by LATTICES: 6;

        then

         A1: j [= k by Def7;

        (j "\/" k) = (k "\/" j);

        hence thesis by A1;

      end;

    end

    theorem :: FILTER_0:28



     Th28: (i => i) = ( Top I)

    proof

      now

        let j;

        (i "/\" j) [= i by LATTICES: 6;

        then j [= (i => i) by Def7;

        hence (j "\/" (i => i)) = (i => i);

      end;

      hence thesis by RLSUB_2: 65;

    end;

    registration

      cluster -> distributive for I_Lattice;

      coherence

      proof

        let I;

        let i, j, k;

        (i "/\" k) [= ((i "/\" k) "\/" (i "/\" j)) by LATTICES: 5;

        then

         A1: k [= (i => ((i "/\" j) "\/" (i "/\" k))) by Def7;

        (i "/\" j) [= ((i "/\" j) "\/" (i "/\" k)) by LATTICES: 5;

        then j [= (i => ((i "/\" j) "\/" (i "/\" k))) by Def7;

        then (j "\/" k) [= (i => ((i "/\" j) "\/" (i "/\" k))) by A1, Th6;

        then

         A2: (i "/\" (j "\/" k)) [= (i "/\" (i => ((i "/\" j) "\/" (i "/\" k)))) by LATTICES: 9;

        (i "/\" j) [= (i "/\" (j "\/" k)) & (i "/\" k) [= (i "/\" (j "\/" k)) by LATTICES: 5, LATTICES: 9;

        then

         A3: ((i "/\" j) "\/" (i "/\" k)) [= (i "/\" (j "\/" k)) by Th6;

        (i "/\" (i => ((i "/\" j) "\/" (i "/\" k)))) [= ((i "/\" j) "\/" (i "/\" k)) by Def7;

        then (i "/\" (j "\/" k)) [= ((i "/\" j) "\/" (i "/\" k)) by A2, LATTICES: 7;

        hence (i "/\" (j "\/" k)) = ((i "/\" j) "\/" (i "/\" k)) by A3, LATTICES: 8;

      end;

    end

    reserve B for B_Lattice,

FB,HB for Filter of B;

    registration

      cluster -> implicative for B_Lattice;

      coherence

      proof

        let B;

        let p,q be Element of B;

        take r = ((p ` ) "\/" q);

        thus (p "/\" r) [= q & for r1 be Element of B st (p "/\" r1) [= q holds r1 [= r by Th27;

      end;

    end

    registration

      cluster implicative -> distributive for Lattice;

      coherence ;

    end

    reserve I for I_Lattice,

i,j,k for Element of I,

DI for non empty Subset of I,

FI for Filter of I;

    theorem :: FILTER_0:29



     Th29: i in FI & (i => j) in FI implies j in FI

    proof

      assume i in FI & (i => j) in FI;

      then

       A1: (i "/\" (i => j)) in FI by Th8;

      (i "/\" (i => j)) [= j by Def7;

      hence thesis by A1, Th9;

    end;

    theorem :: FILTER_0:30



     Th30: j in FI implies (i => j) in FI

    proof

      (j "/\" i) [= j by LATTICES: 6;

      then j [= (i => j) by Def7;

      hence thesis by Th9;

    end;

    definition

      let L, D1, D2;

      :: FILTER_0:def8

      func D1 "/\" D2 -> Subset of L equals { (p "/\" q) : p in D1 & q in D2 };

      coherence

      proof

        set x = the Element of D1, y = the Element of D2;

        reconsider x, y as Element of L;

        (x "/\" y) in { (p "/\" q) : p in D1 & q in D2 };

        then

        reconsider D = { (p "/\" q) : p in D1 & q in D2 } as non empty set;

        D c= the carrier of L

        proof

          let x be object;

          assume x in D;

          then ex p, q st x = (p "/\" q) & p in D1 & q in D2;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let L, D1, D2;

      cluster (D1 "/\" D2) -> non empty;

      coherence

      proof

        set x = the Element of D1, y = the Element of D2;

        reconsider x, y as Element of L;

        (x "/\" y) in { (p "/\" q) : p in D1 & q in D2 };

        hence thesis;

      end;

    end

    theorem :: FILTER_0:31

    p in D1 & q in D2 implies (p "/\" q) in (D1 "/\" D2) & (q "/\" p) in (D1 "/\" D2);

    theorem :: FILTER_0:32

    x in (D1 "/\" D2) implies ex p, q st x = (p "/\" q) & p in D1 & q in D2;

    theorem :: FILTER_0:33



     Th33: (D1 "/\" D2) = (D2 "/\" D1)

    proof

      now

        let D1, D2;

        thus (D1 "/\" D2) c= (D2 "/\" D1)

        proof

          let x be object;

          assume x in (D1 "/\" D2);

          then ex p, q st x = (p "/\" q) & p in D1 & q in D2;

          hence thesis;

        end;

      end;

      hence (D1 "/\" D2) c= (D2 "/\" D1) & (D2 "/\" D1) c= (D1 "/\" D2);

    end;

    registration

      let L be D_Lattice;

      let F1,F2 be Filter of L;

      cluster (F1 "/\" F2) -> final meet-closed;

      coherence

      proof

        now

          let p,q be Element of L;



           A1: p = (p "\/" (p "/\" q)) & q = (q "\/" (p "/\" q)) by LATTICES:def 8;

          thus p in (F1 "/\" F2) & q in (F1 "/\" F2) implies (p "/\" q) in (F1 "/\" F2)

          proof

            assume p in (F1 "/\" F2);

            then

            consider p1,p2 be Element of L such that

             A2: p = (p1 "/\" p2) and

             A3: p1 in F1 & p2 in F2;

            assume q in (F1 "/\" F2);

            then

            consider q1,q2 be Element of L such that

             A4: q = (q1 "/\" q2) and

             A5: q1 in F1 & q2 in F2;



             A6: (p "/\" q) = (((p1 "/\" p2) "/\" q1) "/\" q2) by A2, A4, LATTICES:def 7

            .= (((p1 "/\" q1) "/\" p2) "/\" q2) by LATTICES:def 7

            .= ((p1 "/\" q1) "/\" (p2 "/\" q2)) by LATTICES:def 7;

            (p1 "/\" q1) in F1 & (p2 "/\" q2) in F2 by A3, A5, Th8;

            hence thesis by A6;

          end;

          assume (p "/\" q) in (F1 "/\" F2);

          then

          consider p1,q1 be Element of L such that

           A7: (p "/\" q) = (p1 "/\" q1) and

           A8: p1 in F1 & q1 in F2;



           A9: (q "\/" p1) in F1 & (q "\/" q1) in F2 by A8, Th10;



           A10: (p "\/" (p1 "/\" q1)) = ((p "\/" p1) "/\" (p "\/" q1)) & (q "\/" (p1 "/\" q1)) = ((q "\/" p1) "/\" (q "\/" q1)) by LATTICES: 11;

          (p "\/" p1) in F1 & (p "\/" q1) in F2 by A8, Th10;

          hence p in (F1 "/\" F2) & q in (F1 "/\" F2) by A7, A1, A10, A9;

        end;

        hence thesis by Th8;

      end;

    end

    theorem :: FILTER_0:34



     Th34: <.(D1 \/ D2).) = <.( <.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).)

    proof

      now

        let D1, D2;

        D2 c= (D1 \/ D2) & (D1 \/ D2) c= <.(D1 \/ D2).) by Def4, XBOOLE_1: 7;

        then

         A1: D2 c= <.(D1 \/ D2).);

        D1 c= <.D1.) by Def4;

        then (D1 \/ D2) c= ( <.D1.) \/ D2) by XBOOLE_1: 9;

        hence <.(D1 \/ D2).) c= <.( <.D1.) \/ D2).) by Th22;

         <.D1.) c= <.(D1 \/ D2).) by Th22, XBOOLE_1: 7;

        then ( <.D1.) \/ D2) c= <.(D1 \/ D2).) by A1, XBOOLE_1: 8;

        hence <.( <.D1.) \/ D2).) c= <.(D1 \/ D2).) by Def4;

      end;

      hence <.(D1 \/ D2).) c= <.( <.D1.) \/ D2).) & <.( <.D1.) \/ D2).) c= <.(D1 \/ D2).) & <.(D1 \/ D2).) c= <.(D1 \/ <.D2.)).) & <.(D1 \/ <.D2.)).) c= <.(D1 \/ D2).);

    end;

    theorem :: FILTER_0:35

     <.(F \/ H).) = { r : ex p, q st (p "/\" q) [= r & p in F & q in H }

    proof

      set X = { r1 : ex p, q st (p "/\" q) [= r1 & p in F & q in H };

      consider p1 such that

       A1: p1 in F by SUBSET_1: 4;

      consider q1 such that

       A2: q1 in H by SUBSET_1: 4;

      (p1 "/\" q1) in X by A1, A2;

      then

      reconsider D = X as non empty set;

      D c= the carrier of L

      proof

        let x be object;

        assume x in D;

        then ex r1 st x = r1 & ex p, q st (p "/\" q) [= r1 & p in F & q in H;

        hence thesis;

      end;

      then

      reconsider D as non empty Subset of L;



       A3: for p, q st p in D & p [= q holds q in D

      proof

        let p, q;

        assume p in D;

        then ex r1 st p = r1 & ex p, q st (p "/\" q) [= r1 & p in F & q in H;

        then

        consider p1, q1 such that

         A4: (p1 "/\" q1) [= p and

         A5: p1 in F & q1 in H;

        assume p [= q;

        then (p1 "/\" q1) [= q by A4, LATTICES: 7;

        hence thesis by A5;

      end;

      for p, q st p in D & q in D holds (p "/\" q) in D

      proof

        let p, q;

        assume p in D;

        then ex r1 be Element of L st p = r1 & ex p, q st (p "/\" q) [= r1 & p in F & q in H;

        then

        consider p1,q1 be Element of L such that

         A6: (p1 "/\" q1) [= p and

         A7: p1 in F & q1 in H;

        assume q in D;

        then ex r2 be Element of L st q = r2 & ex p, q st (p "/\" q) [= r2 & p in F & q in H;

        then

        consider p2,q2 be Element of L such that

         A8: (p2 "/\" q2) [= q and

         A9: p2 in F & q2 in H;



         A10: (p "/\" (p2 "/\" q2)) [= (p "/\" q) by A8, LATTICES: 9;

        ((p1 "/\" q1) "/\" (p2 "/\" q2)) [= (p "/\" (p2 "/\" q2)) by A6, LATTICES: 9;

        then

         A11: ((p1 "/\" q1) "/\" (p2 "/\" q2)) [= (p "/\" q) by A10, LATTICES: 7;



         A12: ((p1 "/\" q1) "/\" (p2 "/\" q2)) = (((p1 "/\" q1) "/\" p2) "/\" q2) by LATTICES:def 7

        .= (((p1 "/\" p2) "/\" q1) "/\" q2) by LATTICES:def 7

        .= ((p1 "/\" p2) "/\" (q1 "/\" q2)) by LATTICES:def 7;

        (p1 "/\" p2) in F & (q1 "/\" q2) in H by A7, A9, Th8;

        hence thesis by A12, A11;

      end;

      then

      reconsider D as Filter of L by A3, Th9;



       A13: H c= D

      proof

        let x be object;

        assume x in H;

        then

        reconsider q = x as Element of H;

        (q "/\" p1) [= q by LATTICES: 6;

        hence thesis by A1;

      end;

      F c= D

      proof

        let x be object;

        assume x in F;

        then

        reconsider p = x as Element of F;

        (p "/\" q1) [= p by LATTICES: 6;

        hence thesis by A2;

      end;

      then (F \/ H) c= D by A13, XBOOLE_1: 8;

      hence <.(F \/ H).) c= X by Def4;

      let x be object;

      assume x in X;

      then

      consider r such that

       A14: x = r and

       A15: ex p, q st (p "/\" q) [= r & p in F & q in H;



       A16: (F \/ H) c= <.(F \/ H).) by Def4;

      H c= (F \/ H) by XBOOLE_1: 7;

      then

       A17: H c= <.(F \/ H).) by A16;

      consider p, q such that

       A18: (p "/\" q) [= r and

       A19: p in F & q in H by A15;

      F c= (F \/ H) by XBOOLE_1: 7;

      then F c= <.(F \/ H).) by A16;

      then (p "/\" q) in <.(F \/ H).) by A19, A17, Th8;

      hence thesis by A14, A18, Th9;

    end;

    theorem :: FILTER_0:36



     Th36: F c= (F "/\" H) & H c= (F "/\" H)

    proof

       A1:

      now

        let F, H;

        thus F c= (F "/\" H)

        proof

          let x be object;

          assume

           A2: x in F;

          then

          reconsider i = x as Element of L;

          consider p such that

           A3: p in H by SUBSET_1: 4;

          i [= (i "\/" p) by LATTICES: 5;

          then

           A4: (i "/\" (i "\/" p)) = i by LATTICES: 4;

          p [= (p "\/" i) by LATTICES: 5;

          then (i "\/" p) in H by A3, Th9;

          hence thesis by A2, A4;

        end;

      end;

      (F "/\" H) = (H "/\" F) by Th33;

      hence thesis by A1;

    end;

    theorem :: FILTER_0:37



     Th37: <.(F \/ H).) = <.(F "/\" H).)

    proof

      F c= (F "/\" H) & H c= (F "/\" H) by Th36;

      then (F \/ H) c= (F "/\" H) by XBOOLE_1: 8;

      hence <.(F \/ H).) c= <.(F "/\" H).) by Th22;

      (F "/\" H) c= <.(F \/ H).)

      proof

        let x be object;

        assume x in (F "/\" H);

        then

        consider p, q such that

         A1: x = (p "/\" q) and

         A2: p in F and

         A3: q in H;

        H c= (F \/ H) by XBOOLE_1: 7;

        then

         A4: q in (F \/ H) by A3;



         A5: (F \/ H) c= <.(F \/ H).) by Def4;

        F c= (F \/ H) by XBOOLE_1: 7;

        then p in (F \/ H) by A2;

        hence thesis by A1, A4, A5, Th9;

      end;

      then <.(F "/\" H).) c= <. <.(F \/ H).).) by Th22;

      hence thesis by Th21;

    end;

    reserve F1,F2 for Filter of I;

    theorem :: FILTER_0:38



     Th38: <.(F1 \/ F2).) = (F1 "/\" F2)

    proof

      (F1 "/\" F2) = <.(F1 "/\" F2).) by Th21;

      hence thesis by Th37;

    end;

    theorem :: FILTER_0:39

     <.(FB \/ HB).) = (FB "/\" HB)

    proof

      (FB "/\" HB) = <.(FB "/\" HB).) by Th21;

      hence thesis by Th37;

    end;

    theorem :: FILTER_0:40



     Th40: j in <.(DI \/ {i}).) implies (i => j) in <.DI.)

    proof

      assume

       A1: j in <.(DI \/ {i}).);

       <.(DI \/ {i}).) = <.( <.DI.) \/ {i}).) by Th34

      .= <.( <.DI.) \/ <. {i}.)).) by Th34

      .= <.( <.DI.) \/ <.i.)).) by Th24

      .= ( <.DI.) "/\" <.i.)) by Th38;

      then

      consider i1,i2 be Element of I such that

       A2: j = (i1 "/\" i2) and

       A3: i1 in <.DI.) and

       A4: i2 in <.i.) by A1;

      i [= i2 by A4, Th15;

      then (i1 "/\" i) [= (i1 "/\" i2) by LATTICES: 9;

      then i1 [= (i => j) by A2, Def7;

      hence thesis by A3, Th9;

    end;

    theorem :: FILTER_0:41



     Th41: (i => j) in FI & (j => k) in FI implies (i => k) in FI

    proof

      assume that

       A1: (i => j) in FI and

       A2: (j => k) in FI;



       A3: (FI \/ {i}) c= <.(FI \/ {i}).) by Def4;

       {i} c= (FI \/ {i}) by XBOOLE_1: 7;

      then

       A4: {i} c= <.(FI \/ {i}).) by A3;

      FI c= (FI \/ {i}) by XBOOLE_1: 7;

      then

       A5: FI c= <.(FI \/ {i}).) by A3;

      i in {i} by TARSKI:def 1;

      then j in <.(FI \/ {i}).) by A1, A5, A4, Th29;

      then

       A6: k in <.(FI \/ {i}).) by A2, A5, Th29;

       <.FI.) = FI by Th21;

      hence thesis by A6, Th40;

    end;

    reserve a,b,c for Element of B;

    theorem :: FILTER_0:42



     Th42: (a => b) = ((a ` ) "\/" b)

    proof

      (a "/\" ((a ` ) "\/" b)) [= b & for c st (a "/\" c) [= b holds c [= ((a ` ) "\/" b) by Th27;

      hence thesis by Def7;

    end;

    theorem :: FILTER_0:43



     Th43: a [= b iff (a "/\" (b ` )) = ( Bottom B)

    proof

      reconsider B9 = B as 0_Lattice;

      reconsider B99 = B as 1_Lattice;

      reconsider D = B as D_Lattice;

      reconsider a9 = a, b9 = b, c9 = (a "/\" (b ` )) as Element of B9;

      reconsider a99 = a, b99 = b as Element of B99;

      reconsider a1 = a, b1 = b as Element of D;

      thus a [= b implies (a "/\" (b ` )) = ( Bottom B)

      proof

        assume a [= b;

        then a = (a "/\" b) by LATTICES: 4;



        hence (a "/\" (b ` )) = (a "/\" (b "/\" (b ` ))) by LATTICES:def 7

        .= (a9 "/\" ( Bottom B9)) by LATTICES: 20

        .= ( Bottom B);

      end;

      assume (a "/\" (b ` )) = ( Bottom B);



      then b = (b9 "\/" c9)

      .= ((b1 "\/" a1) "/\" (b1 "\/" (b1 ` ))) by LATTICES: 11

      .= ((b99 "\/" a99) "/\" ( Top B99)) by LATTICES: 21

      .= (a "\/" b);

      hence thesis;

    end;

    theorem :: FILTER_0:44



     Th44: FB is being_ultrafilter iff FB <> the carrier of B & for a holds a in FB or (a ` ) in FB

    proof

      thus FB is being_ultrafilter implies FB <> the carrier of B & for a holds a in FB or (a ` ) in FB

      proof

        reconsider I = B as I_Lattice;

        assume that

         A1: FB <> the carrier of B and

         A2: for HB st FB c= HB & HB <> the carrier of B holds FB = HB;

        thus FB <> the carrier of B by A1;

        let a such that

         A3: not a in FB;



         A4: a in <.a.);



         A5: (FB \/ <.a.)) c= <.(FB \/ <.a.)).) by Def4;

         <.a.) c= (FB \/ <.a.)) by XBOOLE_1: 7;

        then <.a.) c= <.(FB \/ <.a.)).) by A5;

        then FB c= (FB \/ <.a.)) & FB <> <.(FB \/ <.a.)).) by A3, A4, XBOOLE_1: 7;

        then <.(FB \/ <.a.)).) = the carrier of B by A2, A5, XBOOLE_1: 1;

        then

         A6: (a ` ) in <.(FB \/ <.a.)).);

        reconsider a9 = a as Element of I;

        reconsider FI = FB as Filter of I;



         A7: (a => (a ` )) = ((a ` ) "\/" (a ` )) by Th42;

         <. {a}.) = <.a.) by Th24;

        then

         A8: (a9 ` ) in <.(FI \/ {a9}).) by A6, Th34;

        FB = <.FB.) by Th21;

        then (a => (a ` )) in FB by A8, Th40;

        hence thesis by A7;

      end;

      assume that

       A9: FB <> the carrier of B and

       A10: for a holds a in FB or (a ` ) in FB;

      thus FB <> the carrier of B by A9;

      let HB;

      assume that

       A11: FB c= HB and

       A12: HB <> the carrier of B and

       A13: FB <> HB;

      ex x be object st not (x in FB iff x in HB) by A13, TARSKI: 2;

      then

      consider x such that

       A14: x in HB and

       A15: not x in FB by A11;

      reconsider x as Element of HB by A14;

      (x ` ) in FB by A10, A15;

      then ((x ` ) "/\" x) in HB by A11, Th8;

      then

       A16: ( Bottom B) in HB by LATTICES: 20;

      HB = <.HB.) by Th21;

      hence contradiction by A12, A16, Th25;

    end;

    theorem :: FILTER_0:45

    FB <> <.B.) & FB is prime iff FB is being_ultrafilter

    proof

      thus FB <> <.B.) & FB is prime implies FB is being_ultrafilter

      proof

        assume that

         A1: FB <> <.B.) and

         A2: for a, b holds (a "\/" b) in FB iff a in FB or b in FB;

        now

          let a such that

           A3: not a in FB;

          (a "\/" (a ` )) = ( Top B) by LATTICES: 21;

          then (a "\/" (a ` )) in FB by Th11;

          hence (a ` ) in FB by A2, A3;

        end;

        hence thesis by A1, Th44;

      end;

      assume

       A4: FB is being_ultrafilter;

      hence FB <> <.B.);

      let a, b;



       A5: FB <> the carrier of B by A4;

      thus (a "\/" b) in FB implies a in FB or b in FB

      proof

        assume that

         A6: (a "\/" b) in FB and

         A7: ( not a in FB) & not b in FB;

        (a ` ) in FB & (b ` ) in FB by A4, A7, Th44;

        then ((a ` ) "/\" (b ` )) in FB by Th8;

        then ((a "\/" b) ` ) in FB by LATTICES: 24;

        then ((a "\/" b) "/\" ((a "\/" b) ` )) in FB by A6, Th8;

        then

         A8: ( Bottom B) in FB by LATTICES: 20;

        FB = <.FB.) by Th21;

        hence contradiction by A5, A8, Th25;

      end;

      thus thesis by Th10;

    end;

    theorem :: FILTER_0:46



     Th46: FB is being_ultrafilter implies for a holds a in FB iff not (a ` ) in FB

    proof

      assume

       A1: FB is being_ultrafilter;

      let a;

      thus a in FB implies not (a ` ) in FB

      proof

        assume a in FB & (a ` ) in FB;

        then (a "/\" (a ` )) in FB by Th8;

        then ( Bottom B) in FB by LATTICES: 20;

        then FB = the carrier of B by Th26;

        hence contradiction by A1;

      end;

      thus thesis by A1, Th44;

    end;

    theorem :: FILTER_0:47

    a <> b implies ex FB st FB is being_ultrafilter & (a in FB & not b in FB or not a in FB & b in FB)

    proof

      assume a <> b;

      then not a [= b or not b [= a by LATTICES: 8;

      then (a "/\" (b ` )) <> ( Bottom B) or (b "/\" (a ` )) <> ( Bottom B) by Th43;

      then (ex FB st (a "/\" (b ` )) in FB & FB is being_ultrafilter) or ex FB st (b "/\" (a ` )) in FB & FB is being_ultrafilter by Th20;

      then

      consider FB such that

       A1: FB is being_ultrafilter and

       A2: (a "/\" (b ` )) in FB or (b "/\" (a ` )) in FB;

      take FB;

      thus FB is being_ultrafilter by A1;

      a in FB & (b ` ) in FB or b in FB & (a ` ) in FB by A2, Th8;

      hence thesis by A1, Th46;

    end;

    reserve o1,o2 for BinOp of F;

    definition

      let L, F;

      :: FILTER_0:def9

      func latt F -> Lattice means

      : Def9: ex o1, o2 st o1 = (the L_join of L || F) & o2 = (the L_meet of L || F) & it = LattStr (# F, o1, o2 #);

      uniqueness ;

      existence

      proof

        reconsider o1 = (the L_join of L || F), o2 = (the L_meet of L || F) as Function of [:F, F:], the carrier of L by FUNCT_2: 32;



         A1: ( dom o1) = [:F, F:] by FUNCT_2:def 1;

        ( rng o1) c= F

        proof

          let y be object;

          assume y in ( rng o1);

          then

          consider x be object such that

           A2: x in ( dom o1) and

           A3: y = (o1 . x) by FUNCT_1:def 3;

          reconsider p = (x `1 ), q = (x `2 ) as Element of F by A2, MCART_1: 10;

          x = [(x `1 ), (x `2 )] by A2, MCART_1: 21;

          then (o1 . x) = (p "\/" q) by A2, FUNCT_1: 47;

          hence thesis by A3, Th10;

        end;

        then

        reconsider o1 as Function of [:F, F qua non empty set:], F by A1, FUNCT_2:def 1, RELSET_1: 4;



         A4: ( dom o2) = [:F, F:] by FUNCT_2:def 1;

        ( rng o2) c= F

        proof

          let y be object;

          assume y in ( rng o2);

          then

          consider x be object such that

           A5: x in ( dom o2) and

           A6: y = (o2 . x) by FUNCT_1:def 3;

          reconsider p = (x `1 ), q = (x `2 ) as Element of F by A5, MCART_1: 10;

          x = [(x `1 ), (x `2 )] by A5, MCART_1: 21;

          then (o2 . x) = (p "/\" q) by A5, FUNCT_1: 47;

          hence thesis by A6, Th8;

        end;

        then

        reconsider o2 as Function of [:F, F qua non empty set:], F by A4, FUNCT_2:def 1, RELSET_1: 4;

        reconsider K = LattStr (# F, o1, o2 #) as non empty LattStr;



         A7: for a,b be Element of K holds (the L_join of K . (a,b)) = (the L_join of L . (a,b)) & (the L_meet of K . (a,b)) = (the L_meet of L . (a,b))

        proof

          let a,b be Element of K;

          (the L_join of K . (a,b)) = (the L_join of K . [a, b]);

          hence thesis by A1, A4, FUNCT_1: 47;

        end;



         A8: for a,b,c be Element of K holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

        proof

          let a,b,c be Element of K;

          reconsider a9 = a, b9 = b, c9 = c as Element of F;



          thus (a "/\" (b "/\" c)) = (the L_meet of L . (a,(b "/\" c))) by A7

          .= (a9 "/\" (b9 "/\" c9)) by A7

          .= ((a9 "/\" b9) "/\" c9) by LATTICES:def 7

          .= (the L_meet of L . ((a "/\" b),c)) by A7

          .= ((a "/\" b) "/\" c) by A7;

        end;



         A9: for a,b be Element of K holds (a "/\" (a "\/" b)) = a

        proof

          let a,b be Element of K;

          reconsider a9 = a, b9 = b as Element of F;



          thus (a "/\" (a "\/" b)) = (the L_meet of L . (a,(a "\/" b))) by A7

          .= (a9 "/\" (a9 "\/" b9)) by A7

          .= a by LATTICES:def 9;

        end;



         A10: for a,b be Element of K holds (a "/\" b) = (b "/\" a)

        proof

          let a,b be Element of K;

          reconsider a9 = a, b9 = b as Element of F;



          thus (a "/\" b) = (the L_meet of L . (a9,b9)) by A7

          .= (b9 "/\" a9) by LATTICES:def 2

          .= (b "/\" a) by A7;

        end;



         A11: for a,b be Element of K holds ((a "/\" b) "\/" b) = b

        proof

          let a,b be Element of K;

          reconsider a9 = a, b9 = b as Element of F;



          thus ((a "/\" b) "\/" b) = (the L_join of L . ((a "/\" b),b)) by A7

          .= ((a9 "/\" b9) "\/" b9) by A7

          .= b by LATTICES:def 8;

        end;



         A12: for a,b be Element of K holds (a "\/" b) = (b "\/" a)

        proof

          let a,b be Element of K;

          reconsider a9 = a, b9 = b as Element of F;



          thus (a "\/" b) = (the L_join of L . (a9,b9)) by A7

          .= (b9 "\/" a9) by LATTICES:def 1

          .= (b "\/" a) by A7;

        end;

        for a,b,c be Element of K holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

        proof

          let a,b,c be Element of K;

          reconsider a9 = a, b9 = b, c9 = c as Element of F;



          thus (a "\/" (b "\/" c)) = (the L_join of L . (a,(b "\/" c))) by A7

          .= (a9 "\/" (b9 "\/" c9)) by A7

          .= ((a9 "\/" b9) "\/" c9) by LATTICES:def 5

          .= (the L_join of L . ((a "\/" b),c)) by A7

          .= ((a "\/" b) "\/" c) by A7;

        end;

        then K is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A12, A11, A10, A8, A9;

        then

        reconsider Q = K as Lattice;

        take Q, o1, o2;

        thus thesis;

      end;

    end

    registration

      let L, F;

      cluster ( latt F) -> strict;

      coherence

      proof

        ex o1, o2 st o1 = (the L_join of L || F) & o2 = (the L_meet of L || F) & ( latt F) = LattStr (# F, o1, o2 #) by Def9;

        hence thesis;

      end;

    end

    theorem :: FILTER_0:48

    for L be strict Lattice holds ( latt <.L.)) = L

    proof

      let L be strict Lattice;

      ( dom the L_meet of L) = [:the carrier of L, the carrier of L:] by FUNCT_2:def 1;

      then

       A1: the L_meet of L = (the L_meet of L || the carrier of L) by RELAT_1: 68;

      ( dom the L_join of L) = [:the carrier of L, the carrier of L:] by FUNCT_2:def 1;

      then the L_join of L = (the L_join of L || the carrier of L) by RELAT_1: 68;

      hence thesis by A1, Def9;

    end;

    theorem :: FILTER_0:49



     Th49: the carrier of ( latt F) = F & the L_join of ( latt F) = (the L_join of L || F) & the L_meet of ( latt F) = (the L_meet of L || F)

    proof

      ex o1, o2 st o1 = (the L_join of L || F) & o2 = (the L_meet of L || F) & ( latt F) = LattStr (# F, o1, o2 #) by Def9;

      hence thesis;

    end;

    theorem :: FILTER_0:50



     Th50: for p9,q9 be Element of ( latt F) st p = p9 & q = q9 holds (p "\/" q) = (p9 "\/" q9) & (p "/\" q) = (p9 "/\" q9)

    proof

      let p9,q9 be Element of ( latt F) such that

       A1: p = p9 & q = q9;

      consider o1, o2 such that

       A2: o1 = (the L_join of L || F) and

       A3: o2 = (the L_meet of L || F) and

       A4: ( latt F) = LattStr (# F, o1, o2 #) by Def9;

      ( dom o1) = [:F, F:] by FUNCT_2:def 1;

      then [p, q] in ( dom o1) by A1, A4, ZFMISC_1: 87;

      hence (p "\/" q) = (p9 "\/" q9) by A1, A2, A4, FUNCT_1: 47;

      ( dom o2) = [:F, F:] by FUNCT_2:def 1;

      then [p, q] in ( dom o2) by A1, A4, ZFMISC_1: 87;

      hence thesis by A1, A3, A4, FUNCT_1: 47;

    end;

    theorem :: FILTER_0:51



     Th51: for p9,q9 be Element of ( latt F) st p = p9 & q = q9 holds p [= q iff p9 [= q9 by Th50;

    theorem :: FILTER_0:52



     Th52: L is upper-bounded implies ( latt F) is upper-bounded

    proof

      given p such that

       A1: (p "\/" q) = p & (q "\/" p) = p;

      consider q such that

       A2: q in F by SUBSET_1: 4;



       A3: ex o1, o2 st o1 = (the L_join of L || F) & o2 = (the L_meet of L || F) & ( latt F) = LattStr (# F, o1, o2 #) by Def9;

      (p "\/" q) = p by A1;

      then

      reconsider p9 = p as Element of ( latt F) by A2, A3, Th10;

      take p9;

      let r be Element of ( latt F);

      reconsider r9 = r as Element of F by A3;



      thus (p9 "\/" r) = (p "\/" r9) by Th50

      .= p9 by A1;

      hence thesis;

    end;

    theorem :: FILTER_0:53

    L is modular implies ( latt F) is modular

    proof

      assume

       A1: for a,b,c be Element of L st a [= c holds (a "\/" (b "/\" c)) = ((a "\/" b) "/\" c);

      let a,b,c be Element of ( latt F) such that

       A2: a [= c;

      reconsider p = a, q = b, r = c as Element of F by Th49;

      (b "/\" c) = (q "/\" r) by Th50;

      then

       A3: (a "\/" (b "/\" c)) = (p "\/" (q "/\" r)) by Th50;

      (a "\/" b) = (p "\/" q) by Th50;

      then

       A4: ((a "\/" b) "/\" c) = ((p "\/" q) "/\" r) by Th50;

      p [= r by A2, Th51;

      hence (a "\/" (b "/\" c)) = ((a "\/" b) "/\" c) by A1, A3, A4;

    end;

    theorem :: FILTER_0:54



     Th54: L is distributive implies ( latt F) is distributive

    proof

      assume

       A1: for p, q, r holds (p "/\" (q "\/" r)) = ((p "/\" q) "\/" (p "/\" r));

      let p9,q9,r9 be Element of ( latt F);

      reconsider p = p9, q = q9, r = r9, qr = (q9 "\/" r9) as Element of F by Th49;



       A2: (p9 "/\" q9) = (p "/\" q) & (p9 "/\" r9) = (p "/\" r) by Th50;



      thus (p9 "/\" (q9 "\/" r9)) = (p "/\" qr) by Th50

      .= (p "/\" (q "\/" r)) by Th50

      .= ((p "/\" q) "\/" (p "/\" r)) by A1

      .= ((p9 "/\" q9) "\/" (p9 "/\" r9)) by A2, Th50;

    end;

    theorem :: FILTER_0:55

    L is I_Lattice implies ( latt F) is implicative

    proof

      assume

       A1: L is I_Lattice;

      then

      reconsider I = L as I_Lattice;

      reconsider FI = F as Filter of I;

      let p9,q9 be Element of ( latt F);

      reconsider p = p9, q = q9 as Element of F by Th49;

      consider r such that

       A2: (p "/\" r) [= q and

       A3: for r1 st (p "/\" r1) [= q holds r1 [= r by A1, Def6;

      reconsider i = p, j = q as Element of I;



       A4: (i => j) in FI by Th30;

      (i => j) = r by A2, A3, Def7;

      then

      reconsider r9 = r as Element of ( latt F) by A4, Th49;

      take r9;

      (p "/\" r) = (p9 "/\" r9) by Th50;

      hence (p9 "/\" r9) [= q9 by A2, Th51;

      let s9 be Element of ( latt F) such that

       A5: (p9 "/\" s9) [= q9;

      reconsider s = s9 as Element of F by Th49;

      (p "/\" s) = (p9 "/\" s9) by Th50;

      then (p "/\" s) [= q by A5, Th51;

      then s [= r by A3;

      hence thesis by Th51;

    end;

    registration

      let L, p;

      cluster ( latt <.p.)) -> lower-bounded;

      coherence

      proof

        the carrier of ( latt <.p.)) = <.p.) by Th49;

        then

        reconsider p9 = p as Element of ( latt <.p.)) by Th16;

        take p9;

        let q9 be Element of ( latt <.p.));

        reconsider q = q9 as Element of <.p.) by Th49;

        p [= q by Th15;

        then (p "/\" q) = p by LATTICES: 4;

        hence thesis by Th50;

      end;

    end

    theorem :: FILTER_0:56



     Th56: ( Bottom ( latt <.p.))) = p

    proof

      consider q9 be Element of ( latt <.p.)) such that

       A1: for r9 be Element of ( latt <.p.)) holds (q9 "/\" r9) = q9 & (r9 "/\" q9) = q9 by LATTICES:def 13;

      the carrier of ( latt <.p.)) = <.p.) by Th49;

      then

      reconsider p9 = p as Element of ( latt <.p.)) by Th16;

      reconsider q = q9 as Element of <.p.) by Th49;

      (q9 "/\" p9) = q9 by A1;

      then q9 [= p9 by LATTICES: 4;

      then

       A2: q [= p by Th51;



       A3: p [= q by Th15;

      q9 = ( Bottom ( latt <.p.))) by A1, RLSUB_2: 64;

      hence thesis by A2, A3, LATTICES: 8;

    end;

    theorem :: FILTER_0:57



     Th57: L is upper-bounded implies ( Top ( latt <.p.))) = ( Top L)

    proof

      given q such that

       A1: for r holds (q "\/" r) = q & (r "\/" q) = q;

      L is 1_Lattice by A1, LATTICES:def 14;

      then ( Top L) in <.p.) by Th11;

      then

      reconsider q9 = ( Top L) as Element of ( latt <.p.)) by Th49;



       A2: q = ( Top L) by A1, RLSUB_2: 65;

      now

        let r9 be Element of ( latt <.p.));

        reconsider r = r9 as Element of <.p.) by Th49;



        thus (r9 "\/" q9) = (q "\/" r) by A2, Th50

        .= q9 by A1, A2;

      end;

      hence thesis by RLSUB_2: 65;

    end;

    theorem :: FILTER_0:58



     Th58: L is 1_Lattice implies ( latt <.p.)) is bounded by Th52;

    theorem :: FILTER_0:59



     Th59: L is C_Lattice & L is M_Lattice implies ( latt <.p.)) is C_Lattice

    proof

      assume that

       A1: L is C_Lattice and

       A2: L is M_Lattice;

      reconsider B = L as C_Lattice by A1;

      reconsider M = ( latt <.p.)) as 01_Lattice by A1, Th58;

      M is complemented

      proof

        let r9 be Element of M;

        reconsider r = r9 as Element of <.p.) by Th49;

        reconsider p1 = p as Element of B;

        consider q such that

         A3: q is_a_complement_of r by A1, LATTICES:def 19;

        the carrier of ( latt <.p.)) = <.p.) by Th49;

        then

        reconsider q9 = (p "\/" q) as Element of M by Th16;

        take q9;



        thus (q9 "\/" r9) = ((p "\/" q) "\/" r) by Th50

        .= (p "\/" (q "\/" r)) by LATTICES:def 5

        .= (p1 "\/" ( Top B)) by A3

        .= ( Top L)

        .= ( Top M) by A1, Th57;

        hence (r9 "\/" q9) = ( Top M);

        p [= r by Th15;

        then ((p "\/" q) "/\" r) = (p "\/" (q "/\" r)) by A2, LATTICES:def 12;



        hence (q9 "/\" r9) = (p "\/" (q "/\" r)) by Th50

        .= (p1 "\/" ( Bottom B)) by A3

        .= p

        .= ( Bottom M) by Th56;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: FILTER_0:60

    L is B_Lattice implies ( latt <.p.)) is B_Lattice

    proof

      assume L is B_Lattice;

      then ( latt <.p.)) is bounded complemented distributive Lattice by Th54, Th59;

      hence thesis;

    end;

    definition

      let L, p, q;

      :: FILTER_0:def10

      func p <=> q -> Element of L equals ((p => q) "/\" (q => p));

      correctness ;

    end

    theorem :: FILTER_0:61

    (p <=> q) = (q <=> p);

    theorem :: FILTER_0:62



     Th62: (i <=> j) in FI & (j <=> k) in FI implies (i <=> k) in FI

    proof

      assume

       A1: (i <=> j) in FI & (j <=> k) in FI;

      then (j => i) in FI & (k => j) in FI by Th8;

      then

       A2: (k => i) in FI by Th41;

      (i => j) in FI & (j => k) in FI by A1, Th8;

      then (i => k) in FI by Th41;

      hence thesis by A2, Th8;

    end;

    definition

      let L, F;

      :: FILTER_0:def11

      func equivalence_wrt F -> Relation means

      : Def11: ( field it ) c= the carrier of L & for p, q holds [p, q] in it iff (p <=> q) in F;

      existence

      proof

        defpred P[ object, object] means ex p, q st $1 = p & $2 = q & (p <=> q) in F;

        consider R be Relation such that

         A1: for x,y be object holds [x, y] in R iff x in the carrier of L & y in the carrier of L & P[x, y] from RELAT_1:sch 1;

        take R;

        thus ( field R) c= the carrier of L

        proof

          let x be object;

          assume x in ( field R);

          then ex y be object st [x, y] in R or [y, x] in R by WELLSET1: 1;

          hence thesis by A1;

        end;

        let p, q;

        thus [p, q] in R implies (p <=> q) in F

        proof

          assume [p, q] in R;

          then ex p1, q1 st p = p1 & q = q1 & (p1 <=> q1) in F by A1;

          hence thesis;

        end;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let R1,R2 be Relation such that

         A2: ( field R1) c= the carrier of L and

         A3: for p, q holds [p, q] in R1 iff (p <=> q) in F and

         A4: ( field R2) c= the carrier of L and

         A5: for p, q holds [p, q] in R2 iff (p <=> q) in F;

        let x,y be object;

        thus [x, y] in R1 implies [x, y] in R2

        proof

          assume

           A6: [x, y] in R1;

          then x in ( field R1) & y in ( field R1) by RELAT_1: 15;

          then

          reconsider p = x, q = y as Element of L by A2;

          (p <=> q) in F by A3, A6;

          hence thesis by A5;

        end;

        assume

         A7: [x, y] in R2;

        then x in ( field R2) & y in ( field R2) by RELAT_1: 15;

        then

        reconsider p = x, q = y as Element of L by A4;

        (p <=> q) in F by A5, A7;

        hence thesis by A3;

      end;

    end

    theorem :: FILTER_0:63



     Th63: ( equivalence_wrt F) is Relation of the carrier of L

    proof

      ( equivalence_wrt F) c= [:the carrier of L, the carrier of L:]

      proof

        let y,z be object;

        assume [y, z] in ( equivalence_wrt F);

        then

         A1: y in ( field ( equivalence_wrt F)) & z in ( field ( equivalence_wrt F)) by RELAT_1: 15;

        ( field ( equivalence_wrt F)) c= the carrier of L by Def11;

        hence thesis by A1, ZFMISC_1: 87;

      end;

      hence thesis;

    end;

    theorem :: FILTER_0:64



     Th64: L is I_Lattice implies ( equivalence_wrt F) is_reflexive_in the carrier of L

    proof

      assume

       A1: L is I_Lattice;

      let x be object;

      assume x in the carrier of L;

      then

      reconsider p = x as Element of L;

      (p => p) = ( Top L) by A1, Th28;

      then (p <=> p) = ( Top L);

      then (p <=> p) in F by A1, Th11;

      hence thesis by Def11;

    end;

    theorem :: FILTER_0:65



     Th65: ( equivalence_wrt F) is_symmetric_in the carrier of L

    proof

      let x,y be object;

      assume x in the carrier of L & y in the carrier of L;

      then

      reconsider p = x, q = y as Element of L;

      assume [x, y] in ( equivalence_wrt F);

      then (p <=> q) in F by Def11;

      then (q <=> p) in F;

      hence thesis by Def11;

    end;

    theorem :: FILTER_0:66



     Th66: L is I_Lattice implies ( equivalence_wrt F) is_transitive_in the carrier of L

    proof

      assume

       A1: L is I_Lattice;

      let x,y,z be object;

      assume x in the carrier of L & y in the carrier of L & z in the carrier of L;

      then

      reconsider p = x, q = y, r = z as Element of L;

      assume [x, y] in ( equivalence_wrt F) & [y, z] in ( equivalence_wrt F);

      then (p <=> q) in F & (q <=> r) in F by Def11;

      then (p <=> r) in F by A1, Th62;

      hence thesis by Def11;

    end;

    theorem :: FILTER_0:67



     Th67: L is I_Lattice implies ( equivalence_wrt F) is Equivalence_Relation of the carrier of L

    proof

      reconsider R = ( equivalence_wrt F) as Relation of the carrier of L by Th63;



       A1: R is_symmetric_in the carrier of L by Th65;

      assume

       A2: L is I_Lattice;

      then R is_reflexive_in the carrier of L by Th64;

      then

       A3: ( field R) = the carrier of L & ( dom R) = the carrier of L by ORDERS_1: 13;

      R is_transitive_in the carrier of L by A2, Th66;

      hence thesis by A3, A1, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

    end;

    theorem :: FILTER_0:68

    L is I_Lattice implies ( field ( equivalence_wrt F)) = the carrier of L

    proof

      assume L is I_Lattice;

      then ( equivalence_wrt F) is Equivalence_Relation of the carrier of L by Th67;

      hence thesis by ORDERS_1: 12;

    end;

    definition

      let I, FI;

      :: original: equivalence_wrt

      redefine

      func equivalence_wrt FI -> Equivalence_Relation of the carrier of I ;

      coherence by Th67;

    end

    definition

      let B, FB;

      :: original: equivalence_wrt

      redefine

      func equivalence_wrt FB -> Equivalence_Relation of the carrier of B ;

      coherence by Th67;

    end

    definition

      let L, F, p, q;

      :: FILTER_0:def12

      pred p,q are_equivalence_wrt F means (p <=> q) in F;

    end

    theorem :: FILTER_0:69

    (p,q) are_equivalence_wrt F iff [p, q] in ( equivalence_wrt F) by Def11;

    theorem :: FILTER_0:70

    (i,i) are_equivalence_wrt FI & (a,a) are_equivalence_wrt FB

    proof



       A1: (a => a) = ( Top B) by Th28;

      (i => i) = ( Top I) & (( Top I) "/\" ( Top I)) = ( Top I) by Th28;

      hence (i <=> i) in FI & (a <=> a) in FB by A1, Th11;

    end;

    theorem :: FILTER_0:71

    (p,q) are_equivalence_wrt F implies (q,p) are_equivalence_wrt F;

    theorem :: FILTER_0:72

    ((i,j) are_equivalence_wrt FI & (j,k) are_equivalence_wrt FI implies (i,k) are_equivalence_wrt FI) & ((a,b) are_equivalence_wrt FB & (b,c) are_equivalence_wrt FB implies (a,c) are_equivalence_wrt FB) by Th62;

    begin

    theorem :: FILTER_0:73

    for L be meet-absorbing meet-commutative meet-associative join-absorbing join-commutative non empty LattStr holds for x,y,z be Element of L st z [= x & z [= y & for z9 be Element of L st z9 [= x & z9 [= y holds z9 [= z holds z = (x "/\" y)

    proof

      let L be meet-absorbing meet-commutative meet-associative join-absorbing join-commutative non empty LattStr;

      let x,y,z be Element of L such that

       A1: z [= x & z [= y and

       A2: for z9 be Element of L st z9 [= x & z9 [= y holds z9 [= z;

      (x "/\" y) [= x & (x "/\" y) [= y by LATTICES: 6;

      then

       A3: (x "/\" y) [= z by A2;

      z [= (x "/\" y) by A1, Th7;

      hence thesis by A3, LATTICES: 8;

    end;

    theorem :: FILTER_0:74

    for L be meet-absorbing meet-commutative join-associative join-absorbing join-commutative non empty LattStr holds for x,y,z be Element of L st x [= z & y [= z & for z9 be Element of L st x [= z9 & y [= z9 holds z [= z9 holds z = (x "\/" y)

    proof

      let L be meet-absorbing meet-commutative join-associative join-absorbing join-commutative non empty LattStr;

      let x,y,z be Element of L such that

       A1: x [= z & y [= z and

       A2: for z9 be Element of L st x [= z9 & y [= z9 holds z [= z9;

      x [= (x "\/" y) & y [= (x "\/" y) by LATTICES: 5;

      then

       A3: z [= (x "\/" y) by A2;

      (x "\/" y) [= z by A1, Th6;

      hence thesis by A3, LATTICES: 8;

    end;