filter_2.miz

    begin

    theorem :: FILTER_2:1



     Th1: for D be non empty set, S be non empty Subset of D, f be BinOp of D, g be BinOp of S st g = (f || S) holds (f is commutative implies g is commutative) & (f is idempotent implies g is idempotent) & (f is associative implies g is associative)

    proof

      let D be non empty set, S be non empty Subset of D;

      let f be BinOp of D, g be BinOp of S;



       A1: ( dom g) = [:S, S:] by FUNCT_2:def 1;

      assume

       A2: g = (f || S);

      thus f is commutative implies g is commutative

      proof

        assume

         A3: for a,b be Element of D holds (f . (a,b)) = (f . (b,a));

        let a,b be Element of S qua non empty set;

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

        reconsider a9, b9 as Element of D;



        thus (g . (a,b)) = (f . [a, b]) by A2, A1, FUNCT_1: 47

        .= (f . (a9,b9))

        .= (f . (b9,a9)) by A3

        .= (g . [b, a]) by A2, A1, FUNCT_1: 47

        .= (g . (b,a));

      end;

      thus f is idempotent implies g is idempotent

      proof

        assume

         A4: for a be Element of D holds (f . (a,a)) = a;

        let a be Element of S;



        thus (g . (a,a)) = (f . [a, a]) by A2, A1, FUNCT_1: 47

        .= (f . (a,a))

        .= a by A4;

      end;

      assume

       A5: for a,b,c be Element of D holds (f . ((f . (a,b)),c)) = (f . (a,(f . (b,c))));

      let a,b,c be Element of S qua non empty set;

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

      reconsider a9, b9, c9 as Element of D;



      thus (g . ((g . (a,b)),c)) = (f . [(g . (a,b)), c]) by A2, A1, FUNCT_1: 47

      .= (f . [(f . [a, b]), c]) by A2, A1, FUNCT_1: 47

      .= (f . ((f . (a,b)),c))

      .= (f . (a9,(f . (b9,c9)))) by A5

      .= (f . (a,(g . [b, c]))) by A2, A1, FUNCT_1: 47

      .= (f . [a, (g . (b,c))])

      .= (g . (a,(g . (b,c)))) by A2, A1, FUNCT_1: 47;

    end;

    theorem :: FILTER_2:2

    for D be non empty set, S be non empty Subset of D, f be BinOp of D, g be BinOp of S holds for d be Element of D, d9 be Element of S st g = (f || S) & d9 = d holds (d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g) & (d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g) & (d is_a_unity_wrt f implies d9 is_a_unity_wrt g)

    proof

      let D be non empty set, S be non empty Subset of D, f be BinOp of D;

      let g be BinOp of S, d be Element of D, d9 be Element of S such that

       A1: g = (f || S) and

       A2: d9 = d;



       A3: ( dom g) = [:S, S:] by FUNCT_2:def 1;

      thus d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g

      proof

        assume

         A4: for a be Element of D holds (f . (d,a)) = a;

        let a be Element of S;



        thus (g . (d9,a)) = (f . [d9, a]) by A1, A3, FUNCT_1: 47

        .= (f . (d,a)) by A2

        .= a by A4;

      end;

      thus d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g

      proof

        assume

         A5: for a be Element of D holds (f . (a,d)) = a;

        let a be Element of S;



        thus (g . (a,d9)) = (f . [a, d9]) by A1, A3, FUNCT_1: 47

        .= (f . (a,d)) by A2

        .= a by A5;

      end;

      assume

       A6: d is_a_unity_wrt f;

      now

        let s be Element of S;

        reconsider s9 = s as Element of D;



         A7: ( dom g) = [:S, S:] by FUNCT_2:def 1;

         [d9, s] in [:S, S:];



        hence (g . (d9,s)) = (f . (d,s9)) by A1, A2, A7, FUNCT_1: 47

        .= s by A6, BINOP_1: 3;

         [s, d9] in [:S, S:];



        hence (g . (s,d9)) = (f . (s9,d)) by A1, A2, A7, FUNCT_1: 47

        .= s by A6, BINOP_1: 3;

      end;

      hence thesis by BINOP_1: 3;

    end;

    theorem :: FILTER_2:3



     Th3: for D be non empty set, S be non empty Subset of D, f1,f2 be BinOp of D, g1,g2 be BinOp of S st g1 = (f1 || S) & g2 = (f2 || S) holds (f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2) & (f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2)

    proof

      let D be non empty set, S be non empty Subset of D, f1,f2 be BinOp of D, g1,g2 be BinOp of S such that

       A1: g1 = (f1 || S) and

       A2: g2 = (f2 || S);

      thus f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2

      proof

        assume

         A3: for a,b,c be Element of D holds (f1 . (a,(f2 . (b,c)))) = (f2 . ((f1 . (a,b)),(f1 . (a,c))));

        let a,b,c be Element of S;

        set ab = (g1 . (a,b)), ac = (g1 . (a,c)), bc = (g2 . (b,c));

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



         A4: (f2 . [b9, c9]) = (f2 . (b9,c9)) & (f1 . [a9, b9]) = (f1 . (a9,b9));



         A5: (f1 . [a9, c9]) = (f1 . (a9,c9)) & (f1 . [a, bc]) = (f1 . (a,bc));

        ( dom g2) = [:S, S:] by FUNCT_2:def 1;

        then

         A6: (g2 . [b, c]) = (f2 . [b, c]) & (g2 . [ab, ac]) = (f2 . [ab, ac]) by A2, FUNCT_1: 47;



         A7: (f2 . [ab, ac]) = (f2 . (ab,ac));



         A8: ( dom g1) = [:S, S:] by FUNCT_2:def 1;

        then

         A9: (g1 . [a, bc]) = (f1 . [a, bc]) by A1, FUNCT_1: 47;

        (g1 . [a, b]) = (f1 . [a, b]) & (g1 . [a, c]) = (f1 . [a, c]) by A1, A8, FUNCT_1: 47;

        hence (g1 . (a,(g2 . (b,c)))) = (g2 . ((g1 . (a,b)),(g1 . (a,c)))) by A3, A4, A9, A5, A6, A7;

      end;

      assume

       A10: for a,b,c be Element of D holds (f1 . ((f2 . (a,b)),c)) = (f2 . ((f1 . (a,c)),(f1 . (b,c))));

      let a,b,c be Element of S;

      set ab = (g2 . (a,b)), ac = (g1 . (a,c)), bc = (g1 . (b,c));



       A11: (f2 . [ac, bc]) = (f2 . (ac,bc));



       A12: ( dom g1) = [:S, S:] by FUNCT_2:def 1;

      then

       A13: (g1 . [ab, c]) = (f1 . [ab, c]) by A1, FUNCT_1: 47;

      ( dom g2) = [:S, S:] by FUNCT_2:def 1;

      then

       A14: (g2 . [a, b]) = (f2 . [a, b]) & (g2 . [ac, bc]) = (f2 . [ac, bc]) by A2, FUNCT_1: 47;

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



       A15: (f1 . [b9, c9]) = (f1 . (b9,c9)) & (f2 . [a9, b9]) = (f2 . (a9,b9));



       A16: (f1 . [a9, c9]) = (f1 . (a9,c9)) & (f1 . [ab, c]) = (f1 . (ab,c));

      (g1 . [b, c]) = (f1 . [b, c]) & (g1 . [a, c]) = (f1 . [a, c]) by A1, A12, FUNCT_1: 47;

      hence (g1 . ((g2 . (a,b)),c)) = (g2 . ((g1 . (a,c)),(g1 . (b,c)))) by A10, A15, A13, A16, A14, A11;

    end;

    theorem :: FILTER_2:4

    for D be non empty set, S be non empty Subset of D, f1,f2 be BinOp of D, g1,g2 be BinOp of S st g1 = (f1 || S) & g2 = (f2 || S) holds f1 is_distributive_wrt f2 implies g1 is_distributive_wrt g2

    proof

      let D be non empty set, S be non empty Subset of D, f1,f2 be BinOp of D;

      let g1,g2 be BinOp of S;

      assume g1 = (f1 || S) & g2 = (f2 || S) & f1 is_left_distributive_wrt f2 & f1 is_right_distributive_wrt f2;

      hence g1 is_left_distributive_wrt g2 & g1 is_right_distributive_wrt g2 by Th3;

    end;

    theorem :: FILTER_2:5



     Th5: for D be non empty set, S be non empty Subset of D, f1,f2 be BinOp of D, g1,g2 be BinOp of S st g1 = (f1 || S) & g2 = (f2 || S) holds f1 absorbs f2 implies g1 absorbs g2

    proof

      let D be non empty set, S be non empty Subset of D, f1,f2 be BinOp of D;

      let g1,g2 be BinOp of S;

      assume that

       A1: g1 = (f1 || S) and

       A2: g2 = (f2 || S);

      assume

       A3: for a,b be Element of D holds (f1 . (a,(f2 . (a,b)))) = a;

      let a,b be Element of S;



       A4: ( dom g2) = [:S, S:] by FUNCT_2:def 1;

      ( dom g1) = [:S, S:] by FUNCT_2:def 1;



      hence (g1 . (a,(g2 . (a,b)))) = (f1 . [a, (g2 . (a,b))]) by A1, FUNCT_1: 47

      .= (f1 . [a, (f2 . [a, b])]) by A2, A4, FUNCT_1: 47

      .= (f1 . (a,(f2 . (a,b))))

      .= a by A3;

    end;

    begin

    definition

      let D be non empty set, X1,X2 be Subset of D;

      :: original: =

      redefine

      :: FILTER_2:def1

      pred X1 = X2 means for x be Element of D holds x in X1 iff x in X2;

      compatibility by SUBSET_1: 3;

    end

    deffunc carr( LattStr) = the carrier of $1;

    deffunc join( LattStr) = the L_join of $1;

    deffunc met( LattStr) = the L_meet of $1;

    reserve L for Lattice,

p,q,r for Element of L,

p9,q9,r9 for Element of (L .: ),

x,y for set;

    theorem :: FILTER_2:6

    for L1,L2 be LattStr st the LattStr of L1 = the LattStr of L2 holds (L1 .: ) = (L2 .: );

    theorem :: FILTER_2:7

    ((L .: ) .: ) = the LattStr of L;

    theorem :: FILTER_2:8

    for L1,L2 be non empty LattStr st the LattStr of L1 = the LattStr of L2 holds for a1,b1 be Element of L1, a2,b2 be Element of L2 st a1 = a2 & b1 = b2 holds (a1 "\/" b1) = (a2 "\/" b2) & (a1 "/\" b1) = (a2 "/\" b2) & (a1 [= b1 iff a2 [= b2);

    theorem :: FILTER_2:9



     Th9: for L1,L2 be 0_Lattice st the LattStr of L1 = the LattStr of L2 holds ( Bottom L1) = ( Bottom L2)

    proof

      let L1,L2 be 0_Lattice;

      assume

       A1: the LattStr of L1 = the LattStr of L2;

      then

      reconsider c = ( Bottom L1) as Element of L2;

      now

        let a be Element of L2;

        reconsider b = a as Element of L1 by A1;

        (( Bottom L1) "/\" b) = ( Bottom L1);

        hence (c "/\" a) = c by A1;

        hence (a "/\" c) = c;

      end;

      hence thesis by LATTICES:def 16;

    end;

    theorem :: FILTER_2:10



     Th10: for L1,L2 be 1_Lattice st the LattStr of L1 = the LattStr of L2 holds ( Top L1) = ( Top L2)

    proof

      let L1,L2 be 1_Lattice;

      assume

       A1: the LattStr of L1 = the LattStr of L2;

      then

      reconsider c = ( Top L1) as Element of L2;

      now

        let a be Element of L2;

        reconsider b = a as Element of L1 by A1;

        (( Top L1) "\/" b) = ( Top L1);

        hence (c "\/" a) = c by A1;

        hence (a "\/" c) = c;

      end;

      hence thesis by LATTICES:def 17;

    end;

    theorem :: FILTER_2:11



     Th11: for L1,L2 be C_Lattice st the LattStr of L1 = the LattStr of L2 holds for a1,b1 be Element of L1, a2,b2 be Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds a2 is_a_complement_of b2 by Th9, Th10;

    theorem :: FILTER_2:12

    for L1,L2 be B_Lattice st the LattStr of L1 = the LattStr of L2 holds for a be Element of L1, b be Element of L2 st a = b holds (a ` ) = (b ` )

    proof

      let L1,L2 be B_Lattice such that

       A1: the LattStr of L1 = the LattStr of L2;

      let a be Element of L1, b be Element of L2 such that

       A2: a = b;

      reconsider b9 = (a ` ) as Element of L2 by A1;

      (a ` ) is_a_complement_of a by LATTICES:def 21;

      then b9 is_a_complement_of b by A1, A2, Th11;

      hence thesis by LATTICES:def 21;

    end;

    theorem :: FILTER_2:13

    for X be Subset of L st for p, q holds p in X & q in X iff (p "/\" q) in X holds X is ClosedSubset of L

    proof

      let X be Subset of L such that

       A1: for p, q holds p in X & q in X iff (p "/\" q) in X;

      for p, q holds p in X & q in X implies (p "\/" q) in X

      proof

        let p, q;

        (p "/\" (p "\/" q)) = p by LATTICES:def 9;

        hence thesis by A1;

      end;

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

    end;

    theorem :: FILTER_2:14

    for X be Subset of L st for p, q holds p in X & q in X iff (p "\/" q) in X holds X is ClosedSubset of L

    proof

      let X be Subset of L such that

       A1: for p, q holds p in X & q in X iff (p "\/" q) in X;

      for p, q holds p in X & q in X implies (p "/\" q) in X

      proof

        let p, q;

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

        hence thesis by A1;

      end;

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

    end;

    definition

      let L;

      mode Ideal of L is non empty initial join-closed Subset of L;

    end



     Lm1: for S be non empty Subset of L holds S is Ideal 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 Ideal of L implies for p,q be Element of L holds p in S & q in S iff (p "\/" q) in S by LATTICES: 5, LATTICES:def 22, LATTICES:def 25;

      assume

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

      S is initial

      proof

        let p,q be Element of L such that

         A2: p [= q and

         A3: q in S;

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

        hence p in S by A1, A3;

      end;

      hence thesis by A1, LATTICES:def 25;

    end;

    theorem :: FILTER_2:15



     Th15: for L1,L2 be Lattice st the LattStr of L1 = the LattStr of L2 holds for x st x is Filter of L1 holds x is Filter of L2

    proof

      let L1,L2 be Lattice such that

       A1: the LattStr of L1 = the LattStr of L2;

      let x;

      assume x is Filter of L1;

      then

      reconsider F = x as Filter of L1;

      now

        let a,b be Element of L2;

        reconsider a9 = a, b9 = b as Element of L1 by A1;

        (a "/\" b) = (a9 "/\" b9) by A1;

        hence a in F & b in F iff (a "/\" b) in F by FILTER_0: 8;

      end;

      hence thesis by A1, FILTER_0: 8;

    end;

    theorem :: FILTER_2:16



     Th16: for L1,L2 be Lattice st the LattStr of L1 = the LattStr of L2 holds for x st x is Ideal of L1 holds x is Ideal of L2

    proof

      let L1,L2 be Lattice such that

       A1: the LattStr of L1 = the LattStr of L2;

      let x;

      assume x is Ideal of L1;

      then

      reconsider F = x as Ideal of L1;

      now

        let a,b be Element of L2;

        reconsider a9 = a, b9 = b as Element of L1 by A1;

        (a "\/" b) = (a9 "\/" b9) by A1;

        hence a in F & b in F iff (a "\/" b) in F by Lm1;

      end;

      hence thesis by A1, Lm1;

    end;

    definition

      let L, p;

      :: FILTER_2:def2

      func p .: -> Element of (L .: ) equals p;

      coherence ;

    end

    definition

      let L;

      let p be Element of (L .: );

      :: FILTER_2:def3

      func .: p -> Element of L equals p;

      coherence ;

    end

    theorem :: FILTER_2:17

    ( .: (p .: )) = p & (( .: p9) .: ) = p9;

    theorem :: FILTER_2:18

    (p "/\" q) = ((p .: ) "\/" (q .: )) & (p "\/" q) = ((p .: ) "/\" (q .: )) & (p9 "/\" q9) = (( .: p9) "\/" ( .: q9)) & (p9 "\/" q9) = (( .: p9) "/\" ( .: q9));

    theorem :: FILTER_2:19

    (p [= q iff (q .: ) [= (p .: )) & (p9 [= q9 iff ( .: q9) [= ( .: p9)) by LATTICE2: 38, LATTICE2: 39;

    definition

      let L;

      let X be Subset of L;

      :: FILTER_2:def4

      func X .: -> Subset of (L .: ) equals X;

      coherence ;

    end

    definition

      let L;

      let X be Subset of (L .: );

      :: FILTER_2:def5

      func .: X -> Subset of L equals X;

      coherence ;

    end

    registration

      let L;

      let D be non empty Subset of L;

      cluster (D .: ) -> non empty;

      coherence ;

    end

    registration

      let L;

      let D be non empty Subset of (L .: );

      cluster ( .: D) -> non empty;

      coherence ;

    end

    registration

      let L;

      let S be meet-closed Subset of L;

      cluster (S .: ) -> join-closed;

      coherence

      proof

        (S .: ) is join-closed

        proof

          let p9, q9;

          (p9 "\/" q9) = (( .: p9) "/\" ( .: q9));

          hence thesis by LATTICES:def 24;

        end;

        hence thesis;

      end;

    end

    registration

      let L;

      let S be join-closed Subset of L;

      cluster (S .: ) -> meet-closed;

      coherence

      proof

        (S .: ) is meet-closed

        proof

          let p9, q9;

          (p9 "/\" q9) = (( .: p9) "\/" ( .: q9));

          hence thesis by LATTICES:def 25;

        end;

        hence thesis;

      end;

    end

    registration

      let L;

      let S be meet-closed Subset of (L .: );

      cluster ( .: S) -> join-closed;

      coherence

      proof

        ( .: S) is join-closed

        proof

          let p, q;

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

          hence thesis by LATTICES:def 24;

        end;

        hence thesis;

      end;

    end

    registration

      let L;

      let S be join-closed Subset of (L .: );

      cluster ( .: S) -> meet-closed;

      coherence

      proof

        ( .: S) is meet-closed

        proof

          let p, q;

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

          hence thesis by LATTICES:def 25;

        end;

        hence thesis;

      end;

    end

    registration

      let L;

      let F be final Subset of L;

      cluster (F .: ) -> initial;

      coherence by LATTICE2: 39, LATTICES:def 23;

    end

    registration

      let L;

      let F be initial Subset of L;

      cluster (F .: ) -> final;

      coherence by LATTICE2: 39, LATTICES:def 22;

    end

    registration

      let L;

      let F be final Subset of (L .: );

      cluster ( .: F) -> initial;

      coherence by LATTICE2: 38, LATTICES:def 23;

    end

    registration

      let L;

      let F be initial Subset of (L .: );

      cluster (F .: ) -> final;

      coherence by LATTICE2: 38, LATTICES:def 22;

    end

    theorem :: FILTER_2:20



     Th20: x is Ideal of L iff x is Filter of (L .: )

    proof

      thus x is Ideal of L implies x is Filter of (L .: )

      proof

        assume x is Ideal of L;

        then

        reconsider I = x as Ideal of L;

        reconsider I as non empty Subset of (L .: );

        I is Filter of (L .: )

        proof

          now

            let p9, q9;

            (p9 "/\" q9) = (( .: p9) "\/" ( .: q9));

            hence p9 in I & q9 in I iff (p9 "/\" q9) in I by Lm1;

          end;

          hence thesis by FILTER_0: 8;

        end;

        hence thesis;

      end;

      assume x is Filter of (L .: );

      then

      reconsider F = x as Filter of (L .: );

      reconsider F as non empty Subset of L;

      now

        let p, q;

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

        hence p in F & q in F iff (p "\/" q) in F by FILTER_0: 8;

      end;

      hence thesis by Lm1;

    end;

    theorem :: FILTER_2:21



     Th21: for D be non empty Subset of L holds D is Ideal 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 & q [= p holds q in D

    proof

      let D be non empty Subset of L;

      thus D is Ideal 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 & q [= p holds q in D by Lm1;

      assume

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

      for p, q holds p in D & q in D iff (p "\/" q) in D by A1, LATTICES: 5;

      hence thesis by Lm1;

    end;

    reserve I,J for Ideal of L,

F for Filter of L;

    theorem :: FILTER_2:22



     Th22: p in I implies (p "/\" q) in I & (q "/\" p) in I

    proof

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

      hence thesis by Th21;

    end;

    theorem :: FILTER_2:23

    ex p st p in I

    proof

      set i = the Element of I qua non empty Subset of L;

      i is Element of L;

      hence thesis;

    end;

    theorem :: FILTER_2:24

    L is lower-bounded implies ( Bottom L) in I

    proof

      assume L is lower-bounded;

      then ( Top (L .: )) = ( Bottom L) & (L .: ) is upper-bounded by LATTICE2: 48, LATTICE2: 61;

      then ( Bottom L) in (I .: ) by FILTER_0: 11;

      hence thesis;

    end;

    theorem :: FILTER_2:25

    L is lower-bounded implies {( Bottom L)} is Ideal of L

    proof

      assume L is lower-bounded;

      then ( Top (L .: )) = ( Bottom L) & (L .: ) is upper-bounded by LATTICE2: 48, LATTICE2: 61;

      then {( Bottom L)} is Filter of (L .: ) by FILTER_0: 12;

      hence thesis by Th20;

    end;

    theorem :: FILTER_2:26

     {p} is Ideal of L implies L is lower-bounded

    proof

      assume {p} is Ideal of L;

      then {p} is Filter of (L .: ) by Th20;

      then (L .: ) is upper-bounded by FILTER_0: 13;

      hence thesis by LATTICE2: 48;

    end;

    begin

    theorem :: FILTER_2:27



     Th27: the carrier of L is Ideal of L

    proof

       carr(L) is Filter of (L .: ) by FILTER_0: 14;

      hence thesis by Th20;

    end;

    definition

      let L;

      :: FILTER_2:def6

      func (.L.> -> Ideal of L equals the carrier of L;

      coherence by Th27;

    end

    definition

      let L, p;

      :: FILTER_2:def7

      func (.p.> -> Ideal of L equals { q : q [= p };

      coherence

      proof

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

        p in X;

        then

        reconsider X as non empty set;

        X c= carr(L)

        proof

          let x be object;

          assume x in X;

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

          hence thesis;

        end;

        then

        reconsider X as non empty Subset of L;

        now

          let q, r;

          thus q in X & r in X implies (q "\/" r) in X

          proof

            assume q in X & r in X;

            then (ex r st q = r & r [= p) & ex q st r = q & q [= p;

            then (q "\/" r) [= p by FILTER_0: 6;

            hence thesis;

          end;

          assume (q "\/" r) in X;

          then

           A1: ex s be Element of L st (q "\/" r) = s & s [= p;

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

          then

           A2: q [= p by A1, LATTICES: 7;

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

          then r [= p by A1, LATTICES: 7;

          hence q in X & r in X by A2;

        end;

        hence thesis by Lm1;

      end;

    end

    theorem :: FILTER_2:28



     Th28: q in (.p.> iff q [= p

    proof

      q in (.p.> iff ex r st q = r & r [= p;

      hence thesis;

    end;

    theorem :: FILTER_2:29



     Th29: (.p.> = <.(p .: ).) & (.(p .: ).> = <.p.)

    proof

       (.p.> = ( .: <.(p .: ).))

      proof

        let q;



         A1: (q .: ) in <.(p .: ).) iff (p .: ) [= (q .: ) by FILTER_0: 15;

        q in (.p.> iff q [= p by Th28;

        hence thesis by A1, LATTICE2: 38, LATTICE2: 39;

      end;

      hence (.p.> = <.(p .: ).);

      ( .: (.(p .: ).>) = <.p.)

      proof

        let q;



         A2: q in <.p.) iff p [= q by FILTER_0: 15;

        (q .: ) in (.(p .: ).> iff (q .: ) [= (p .: ) by Th28;

        hence thesis by A2, LATTICE2: 38, LATTICE2: 39;

      end;

      hence thesis;

    end;

    theorem :: FILTER_2:30

    p in (.p.> & (p "/\" q) in (.p.> & (q "/\" p) in (.p.>

    proof

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

      hence thesis;

    end;

    theorem :: FILTER_2:31

    L is upper-bounded implies (.L.> = (.( Top L).>

    proof

      assume

       A1: L is upper-bounded;

      then (L .: ) is lower-bounded by LATTICE2: 49;

      then

       A2: <.(L .: ).) = <.( Bottom (L .: )).) by FILTER_0: 17;

      ( Bottom (L .: )) = (( Top L) .: ) by A1, LATTICE2: 62;

      hence thesis by A2, Th29;

    end;

    definition

      let L, I;

      :: FILTER_2:def8

      attr I is max-ideal means I <> the carrier of L & for J st I c= J & J <> the carrier of L holds I = J;

    end

    theorem :: FILTER_2:32



     Th32: I is max-ideal iff (I .: ) is being_ultrafilter

    proof

      thus I is max-ideal implies (I .: ) is being_ultrafilter

      proof

        assume that

         A1: I <> carr(L) and

         A2: for J st I c= J & J <> carr(L) holds I = J;

        thus (I .: ) <> carr(.:) by A1;

        let F be Filter of (L .: );

        ( .: F) = F;

        hence thesis by A2;

      end;

      assume that

       A3: (I .: ) <> carr(.:) and

       A4: for F be Filter of (L .: ) st (I .: ) c= F & F <> carr(.:) holds (I .: ) = F;

      thus I <> carr(L) by A3;

      let J be Ideal of L;

      (J .: ) = J;

      hence thesis by A4;

    end;

    theorem :: FILTER_2:33

    L is upper-bounded implies for I st I <> the carrier of L holds ex J st I c= J & J is max-ideal

    proof

      assume L is upper-bounded;

      then

       A1: (L .: ) is lower-bounded by LATTICE2: 49;

      let I;

      assume I <> carr(L);

      then

      consider F be Filter of (L .: ) such that

       A2: (I .: ) c= F & F is being_ultrafilter by A1, FILTER_0: 18;

      take ( .: F);

      (( .: F) .: ) = ( .: F);

      hence thesis by A2, Th32;

    end;

    theorem :: FILTER_2:34

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

    proof

      given r such that

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

      (p "\/" r) = ((p .: ) "/\" (r .: ));

      then <.(p .: ).) <> carr(.:) by A1, FILTER_0: 19;

      hence thesis by Th29;

    end;

    theorem :: FILTER_2:35

    L is upper-bounded & p <> ( Top L) implies ex I st p in I & I is max-ideal

    proof

      assume L is upper-bounded;

      then

       A1: (L .: ) is lower-bounded & ( Bottom (L .: )) = ( Top L) by LATTICE2: 49, LATTICE2: 62;

      assume p <> ( Top L);

      then

      consider F be Filter of (L .: ) such that

       A2: (p .: ) in F & F is being_ultrafilter by A1, FILTER_0: 20;

      take ( .: F);

      (( .: F) .: ) = ( .: F);

      hence thesis by A2, Th32;

    end;

    reserve D for non empty Subset of L,

D9 for non empty Subset of (L .: );

    definition

      let L, D;

      :: FILTER_2:def9

      func (.D.> -> Ideal of L means

      : Def9: D c= it & for I st D c= I holds it c= I;

      existence

      proof

        take I = ( .: <.(D .: ).));

        thus D c= I by FILTER_0:def 4;

        let J;

        (J .: ) = J;

        hence thesis by FILTER_0:def 4;

      end;

      uniqueness ;

    end



     Lm2: for L1,L2 be Lattice, D1 be non empty Subset of L1, D2 be non empty Subset of L2 st the LattStr of L1 = the LattStr of L2 & D1 = D2 holds <.D1.) = <.D2.) & (.D1.> = (.D2.>

    proof

      let L1,L2 be Lattice;

      let D1 be non empty Subset of L1, D2 be non empty Subset of L2;

      assume that

       A1: the LattStr of L1 = the LattStr of L2 and

       A2: D1 = D2;



       A3: D1 c= <.D1.) & D2 c= <.D2.) by FILTER_0:def 4;

       <.D1.) is Filter of L2 & <.D2.) is Filter of L1 by A1, Th15;

      hence <.D1.) c= <.D2.) & <.D2.) c= <.D1.) by A2, A3, FILTER_0:def 4;



       A4: D1 c= (.D1.> & D2 c= (.D2.> by Def9;

       (.D1.> is Ideal of L2 & (.D2.> is Ideal of L1 by A1, Th16;

      hence (.D1.> c= (.D2.> & (.D2.> c= (.D1.> by A2, A4, Def9;

    end;

    theorem :: FILTER_2:36



     Th36: <.(D .: ).) = (.D.> & <.D.) = (.(D .: ).> & <.( .: D9).) = (.D9.> & <.D9.) = (.( .: D9).>

    proof



       A1: for L, D holds <.(D .: ).) = (.D.>

      proof

        let L, D;

        ( (.D.> .: ) = (.D.>;

        then

         A2: D c= (.D.> implies <.(D .: ).) c= (.D.> by FILTER_0:def 4;

        ( .: <.(D .: ).)) = <.(D .: ).);

        then D c= <.(D .: ).) implies (.D.> c= <.(D .: ).) by Def9;

        hence thesis by A2, Def9, FILTER_0:def 4;

      end;

       <.((D .: ) .: ).) = <.D.) & <.((( .: D9) .: ) .: ).) = <.( .: D9).) by Lm2;

      hence thesis by A1;

    end;

    theorem :: FILTER_2:37



     Th37: (.I.> = I by Def9;

    reserve D1,D2 for non empty Subset of L,

D19,D29 for non empty Subset of (L .: );

    theorem :: FILTER_2:38

    (D1 c= D2 implies (.D1.> c= (.D2.>) & (. (.D.>.> c= (.D.>

    proof

      D2 c= (.D2.> by Def9;

      then D1 c= D2 implies D1 c= (.D2.>;

      hence thesis by Def9;

    end;

    theorem :: FILTER_2:39

    p in D implies (.p.> c= (.D.>

    proof

       <.(p .: ).) = (.p.> & <.(D .: ).) = (.D.> by Th29, Th36;

      hence thesis by FILTER_0: 23;

    end;

    theorem :: FILTER_2:40

    D = {p} implies (.D.> = (.p.>

    proof

       <.(p .: ).) = (.p.> & <.(D .: ).) = (.D.> by Th29, Th36;

      hence thesis by FILTER_0: 24;

    end;

    theorem :: FILTER_2:41



     Th41: L is upper-bounded & ( Top L) in D implies (.D.> = (.L.> & (.D.> = the carrier of L

    proof

      assume L is upper-bounded;

      then

       A1: (L .: ) is lower-bounded & ( Bottom (L .: )) = ( Top L) by LATTICE2: 49, LATTICE2: 62;

      assume ( Top L) in D;

      then <.(D .: ).) = <.(L .: ).) by A1, FILTER_0: 25;

      hence thesis by Th36;

    end;

    theorem :: FILTER_2:42

    L is upper-bounded & ( Top L) in I implies I = (.L.> & I = the carrier of L

    proof

       (.I.> = I by Th37;

      hence thesis by Th41;

    end;

    definition

      let L, I;

      :: FILTER_2:def10

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

    end

    theorem :: FILTER_2:43



     Th43: I is prime iff (I .: ) is prime

    proof

      thus I is prime implies (I .: ) is prime

      proof

        assume

         A1: (p "/\" q) in I iff p in I or q in I;

        let p9, q9;

        (p9 "\/" q9) = (( .: p9) "/\" ( .: q9));

        hence thesis by A1;

      end;

      assume

       A2: (p9 "\/" q9) in (I .: ) iff p9 in (I .: ) or q9 in (I .: );

      let p, q;

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

      hence thesis by A2;

    end;

    definition

      let L, D1, D2;

      :: FILTER_2:def11

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

      coherence

      proof

        set X = { (p "\/" q) : p in D1 & q in D2 };

        X c= carr(L)

        proof

          let x be object;

          assume x in X;

          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 = { (p "\/" q) : p in D1 & q in D2 };

        set p1 = the Element of D1, p2 = the Element of D2;

        (p1 "\/" p2) in X;

        then

        reconsider X as non empty set;

        X = (D1 "\/" D2);

        hence thesis;

      end;

    end



     Lm3: for L1,L2 be Lattice, D1,E1 be non empty Subset of L1, D2,E2 be non empty Subset of L2 st the LattStr of L1 = the LattStr of L2 & D1 = D2 & E1 = E2 holds (D1 "/\" E1) = (D2 "/\" E2)

    proof

      let L1,L2 be Lattice, D1,E1 be non empty Subset of L1;

      let D2,E2 be non empty Subset of L2 such that

       A1: the LattStr of L1 = the LattStr of L2 and

       A2: D1 = D2 & E1 = E2;

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

      proof

        let x be object;

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

        then

        consider a,b be Element of L1 such that

         A3: x = (a "/\" b) and

         A4: a in D1 & b in E1;

        reconsider a9 = a, b9 = b as Element of L2 by A1;

        x = (a9 "/\" b9) by A1, A3;

        hence thesis by A2, A4;

      end;

      let x be object;

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

      then

      consider a,b be Element of L2 such that

       A5: x = (a "/\" b) and

       A6: a in D2 & b in E2;

      reconsider a9 = a, b9 = b as Element of L1 by A1;

      x = (a9 "/\" b9) by A1, A5;

      hence thesis by A2, A6;

    end;

    theorem :: FILTER_2:44



     Th44: (D1 "\/" D2) = ((D1 .: ) "/\" (D2 .: )) & ((D1 .: ) "\/" (D2 .: )) = (D1 "/\" D2) & (D19 "\/" D29) = (( .: D19) "/\" ( .: D29)) & (( .: D19) "\/" ( .: D29)) = (D19 "/\" D29)

    proof



       A1: for L, D1, D2 holds (D1 "\/" D2) = ((D1 .: ) "/\" (D2 .: ))

      proof

        let L, D1, D2;

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

        proof

          let x be object;

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

          then

          consider p, q such that

           A2: x = (p "\/" q) & p in D1 & q in D2;

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

          hence thesis by A2;

        end;

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

        proof

          let x be object;

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

          then

          consider p9, q9 such that

           A3: x = (p9 "/\" q9) & p9 in D1 & q9 in D2;

          (( .: p9) "\/" ( .: q9)) = (p9 "/\" q9);

          hence thesis by A3;

        end;

      end;



       A4: (( .: D19) .: ) = ( .: D19) & (( .: D29) .: ) = ( .: D29);

      (((D1 .: ) .: ) "/\" ((D2 .: ) .: )) = (D1 "/\" D2) & ((D19 .: ) "/\" (D29 .: )) = (( .: D19) "/\" ( .: D29)) by Lm3;

      hence thesis by A1, A4;

    end;

    theorem :: FILTER_2:45

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

    theorem :: FILTER_2:46

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

    theorem :: FILTER_2:47

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

    proof

      let r;

      thus r in (D1 "\/" D2) implies r in (D2 "\/" D1)

      proof

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

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

        hence thesis;

      end;

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

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

      hence thesis;

    end;

    registration

      let L be D_Lattice;

      let I1,I2 be Ideal of L;

      cluster (I1 "\/" I2) -> initial join-closed;

      coherence

      proof

        reconsider K = (L .: ) as D_Lattice by LATTICE2: 50;

        reconsider J1 = (I1 .: ), J2 = (I2 .: ) as Filter of K;

        (I1 "\/" I2) = ((I1 .: ) "/\" (I2 .: )) & (J1 "/\" J2) = ((J1 "/\" J2) .: ) by Th44;

        hence thesis by Th16;

      end;

    end

    theorem :: FILTER_2:48

     (.(D1 \/ D2).> = (.( (.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).>

    proof



       A1: (.(D1 \/ (.D2.>).> = <.((D1 \/ (.D2.>) .: ).) & (.D2.> = <.(D2 .: ).) by Th36;



       A2: (.(D1 \/ D2).> = <.((D1 \/ D2) .: ).) by Th36;

       (.( (.D1.> \/ D2).> = <.(( (.D1.> \/ D2) .: ).) & (.D1.> = <.(D1 .: ).) by Th36;

      hence thesis by A1, A2, FILTER_0: 34;

    end;

    theorem :: FILTER_2:49

     (.(I \/ J).> = { r : ex p, q st r [= (p "\/" q) & p in I & q in J }

    proof



       A1: (J .: ) = J;

       (.(I \/ J).> = <.((I \/ J) .: ).) & (I .: ) = I by Th36;

      then

       A2: (.(I \/ J).> = { r9 : ex p9, q9 st (p9 "/\" q9) [= r9 & p9 in I & q9 in J } by A1, FILTER_0: 35;

      thus (.(I \/ J).> c= { r : ex p, q st r [= (p "\/" q) & p in I & q in J }

      proof

        let x be object;

        assume x in (.(I \/ J).>;

        then

        consider r9 such that

         A3: x = r9 and

         A4: ex p9, q9 st (p9 "/\" q9) [= r9 & p9 in I & q9 in J by A2;

        consider p9, q9 such that

         A5: (p9 "/\" q9) [= r9 and

         A6: p9 in I & q9 in J by A4;



         A7: (p9 "/\" q9) = (( .: p9) "\/" ( .: q9));

        ( .: r9) [= ( .: (p9 "/\" q9)) by A5, LATTICE2: 39;

        hence thesis by A3, A6, A7;

      end;

      let x be object;

      assume x in { r : ex p, q st r [= (p "\/" q) & p in I & q in J };

      then

      consider r such that

       A8: x = r and

       A9: ex p, q st r [= (p "\/" q) & p in I & q in J;

      consider p, q such that

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

       A11: p in I & q in J by A9;



       A12: (p "\/" q) = ((p .: ) "/\" (q .: ));

      ((p "\/" q) .: ) [= (r .: ) by A10, LATTICE2: 38;

      hence thesis by A2, A8, A11, A12;

    end;

    theorem :: FILTER_2:50

    I c= (I "\/" J) & J c= (I "\/" J)

    proof

      (I "\/" J) = ((I .: ) "/\" (J .: )) by Th44;

      hence thesis by FILTER_0: 36;

    end;

    theorem :: FILTER_2:51

     (.(I \/ J).> = (.(I "\/" J).>

    proof



       A1: (.(I "\/" J).> = <.((I "\/" J) .: ).) by Th36;

       (.(I \/ J).> = <.((I \/ J) .: ).) & ((I .: ) "/\" (J .: )) = (I "\/" J) by Th36, Th44;

      hence thesis by A1, FILTER_0: 37;

    end;

    reserve B for B_Lattice,

IB,JB for Ideal of B,

a,b for Element of B;

    theorem :: FILTER_2:52



     Th52: L is C_Lattice iff (L .: ) is C_Lattice

    proof



       A1: L is upper-bounded iff (L .: ) is lower-bounded by LATTICE2: 49;



       A2: L is lower-bounded iff (L .: ) is upper-bounded by LATTICE2: 48;

      thus L is C_Lattice implies (L .: ) is C_Lattice

      proof

        assume

         A3: L is C_Lattice;

        now

          let p9;

          consider q such that

           A4: q is_a_complement_of ( .: p9) by A3, LATTICES:def 19;

          take r = (q .: );

          (q "\/" ( .: p9)) = ( Top L) by A4;

          then

           A5: ((q .: ) "/\" p9) = ( Top L);

          (q "/\" ( .: p9)) = ( Bottom L) by A4;

          then

           A6: ((q .: ) "\/" p9) = ( Bottom L);

          ( Top (L .: )) = ( Bottom L) & ( Bottom (L .: )) = ( Top L) by A3, LATTICE2: 61, LATTICE2: 62;

          hence r is_a_complement_of p9 by A5, A6;

        end;

        hence thesis by A2, A1, A3, LATTICES:def 19;

      end;

      assume

       A7: (L .: ) is C_Lattice;

      now

        let p;

        consider q9 such that

         A8: q9 is_a_complement_of (p .: ) by A7, LATTICES:def 19;

        (q9 "\/" (p .: )) = ( Top (L .: )) by A8;

        then

         A9: (( .: q9) "/\" p) = ( Top (L .: ));

        take r = ( .: q9);

        L is upper-bounded by A7, LATTICE2: 49;

        then

         A10: ( Bottom (L .: )) = ( Top L) by LATTICE2: 62;

        (q9 "/\" (p .: )) = ( Bottom (L .: )) by A8;

        then

         A11: (( .: q9) "\/" p) = ( Bottom (L .: ));

        L is lower-bounded by A7, LATTICE2: 48;

        then ( Top (L .: )) = ( Bottom L) by LATTICE2: 61;

        hence r is_a_complement_of p by A9, A11, A10;

      end;

      hence thesis by A2, A1, A7, LATTICES:def 19;

    end;

    theorem :: FILTER_2:53



     Th53: L is B_Lattice iff (L .: ) is B_Lattice

    proof



       A1: L is distributive iff (L .: ) is distributive by LATTICE2: 50;

      L is C_Lattice iff (L .: ) is C_Lattice by Th52;

      hence thesis by A1;

    end;

    registration

      let B be B_Lattice;

      cluster (B .: ) -> Boolean Lattice-like;

      coherence by Th53;

    end

    reserve a9 for Element of (B qua Lattice .: );



     Lm4: ((a .: ) ` ) = (a ` )

    proof

      (((a .: ) ` ) "/\" (a .: )) = ( Bottom (B .: )) by LATTICES: 20;

      then

       A1: (( .: ((a .: ) ` )) "\/" ( .: (a .: ))) = ( Top B) by LATTICE2: 62;

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

      then (( .: ((a .: ) ` )) "/\" ( .: (a .: ))) = ( Bottom B) by LATTICE2: 61;

      then ( .: ((a .: ) ` )) is_a_complement_of a by A1;

      hence thesis by LATTICES:def 21;

    end;

    theorem :: FILTER_2:54



     Th54: ((a .: ) ` ) = (a ` ) & (( .: a9) ` ) = (a9 ` )

    proof

      (( .: a9) .: ) = ( .: a9);

      hence thesis by Lm4;

    end;

    theorem :: FILTER_2:55

     (.(IB \/ JB).> = (IB "\/" JB)

    proof

      reconsider FB = (IB .: ), GB = (JB .: ) as Filter of (B .: );



      thus (.(IB \/ JB).> = <.((IB \/ JB) .: ).) by Th36

      .= (FB "/\" GB) by FILTER_0: 39

      .= (IB "\/" JB) by Th44;

    end;

    theorem :: FILTER_2:56

    IB is max-ideal iff IB <> the carrier of B & for a holds a in IB or (a ` ) in IB

    proof

      reconsider FB = (IB .: ) as Filter of (B .: );



       A1: FB is being_ultrafilter iff FB <> carr(.:) & for a be Element of (B .: ) holds a in FB or (a ` ) in FB by FILTER_0: 44;

      thus IB is max-ideal implies IB <> carr(B) & for a holds a in IB or (a ` ) in IB

      proof

        assume

         A2: IB is max-ideal;

        hence IB <> carr(B);

        let a;

        reconsider b = a as Element of (B .: );

        b in FB or (b ` ) in FB & ((a .: ) ` ) = (a ` ) by A1, A2, Th32, Th54;

        hence thesis;

      end;

      assume that

       A3: IB <> carr(B) and

       A4: for a holds a in IB or (a ` ) in IB;

      now

        let a be Element of (B .: );

        reconsider b = a as Element of B;

        b in FB or (b ` ) in FB & (( .: a qua Element of (B qua Lattice .: )) ` ) = (a ` ) by A4, Th54;

        hence a in FB or (a ` ) in FB;

      end;

      hence thesis by A1, A3, Th32;

    end;

    theorem :: FILTER_2:57

    IB <> (.B.> & IB is prime iff IB is max-ideal

    proof

      reconsider F = (IB .: ) as Filter of (B .: );

       <.(B .: ).) = (.B.>;

      then F <> (.B.> & F is prime iff F is being_ultrafilter by FILTER_0: 45;

      hence thesis by Th32, Th43;

    end;

    theorem :: FILTER_2:58

    IB is max-ideal implies for a holds a in IB iff not (a ` ) in IB

    proof

      reconsider FB = (IB .: ) as Filter of (B .: );

      assume IB is max-ideal;

      then

       A1: FB is being_ultrafilter by Th32;

      let a;

      ((a .: ) ` ) = (a ` ) by Lm4;

      hence thesis by A1, FILTER_0: 46;

    end;

    theorem :: FILTER_2:59

    a <> b implies ex IB st IB is max-ideal & (a in IB & not b in IB or not a in IB & b in IB)

    proof

      assume a <> b;

      then

      consider FB be Filter of (B .: ) such that

       A1: FB is being_ultrafilter and

       A2: (a .: ) in FB & not (b .: ) in FB or not (a .: ) in FB & (b .: ) in FB by FILTER_0: 47;

      take IB = ( .: FB qua Filter of (B qua Lattice .: ));

      (IB .: ) = FB;

      hence IB is max-ideal by A1, Th32;

      thus thesis by A2;

    end;

    reserve P for non empty ClosedSubset of L,

o1,o2 for BinOp of P;

    theorem :: FILTER_2:60



     Th60: (the L_join of L || P) is BinOp of P & (the L_meet of L || P) is BinOp of P

    proof

      ( dom join(L)) = [: carr(L), carr(L):] by FUNCT_2:def 1;

      then

       A1: ( dom ( join(L) || P)) = [:P, P:] by RELAT_1: 62;

      ( rng ( join(L) || P)) c= P

      proof

        let x be object;

        assume x in ( rng ( join(L) || P));

        then

        consider y be object such that

         A2: y in [:P, P:] and

         A3: x = (( join(L) || P) . y) by A1, FUNCT_1:def 3;

        consider p1,p2 be Element of P such that

         A4: y = [p1, p2] by A2, DOMAIN_1: 1;

        x = (p1 "\/" p2) by A1, A3, A4, FUNCT_1: 47;

        hence thesis by LATTICES:def 25;

      end;

      hence ( join(L) || P) is BinOp of P by A1, FUNCT_2:def 1, RELSET_1: 4;

      ( dom met(L)) = [: carr(L), carr(L):] by FUNCT_2:def 1;

      then

       A5: ( dom ( met(L) || P)) = [:P, P:] by RELAT_1: 62;

      ( rng ( met(L) || P)) c= P

      proof

        let x be object;

        assume x in ( rng ( met(L) || P));

        then

        consider y be object such that

         A6: y in [:P, P:] and

         A7: x = (( met(L) || P) . y) by A5, FUNCT_1:def 3;

        consider p1,p2 be Element of P such that

         A8: y = [p1, p2] by A6, DOMAIN_1: 1;

        x = (p1 "/\" p2) by A5, A7, A8, FUNCT_1: 47;

        hence thesis by LATTICES:def 24;

      end;

      hence thesis by A5, FUNCT_2:def 1, RELSET_1: 4;

    end;

    theorem :: FILTER_2:61



     Th61: o1 = (the L_join of L || P) & o2 = (the L_meet of L || P) implies o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 by Th1, Th5, LATTICE2: 26, LATTICE2: 27;

    definition

      let L, p, q;

      assume

       A1: p [= q;

      :: FILTER_2:def12

      func [#p,q#] -> non empty ClosedSubset of L equals

      : Def12: { r : p [= r & r [= q };

      coherence

      proof

        set P = { r : p [= r & r [= q };

        p in P by A1;

        then

        reconsider P as non empty set;

        P c= carr(L)

        proof

          let x be object;

          assume x in P;

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

          hence thesis;

        end;

        then

        reconsider P as non empty Subset of L;

        now

          let p1,p2 be Element of L;

          assume that

           A2: p1 in P and

           A3: p2 in P;



           A4: ex r st p1 = r & p [= r & r [= q by A2;

          then

           A5: p [= (p1 "\/" p2) & (p1 "/\" p2) [= q by FILTER_0: 2, FILTER_0: 3;

          ex r st p2 = r & p [= r & r [= q by A3;

          then p [= (p1 "/\" p2) & (p1 "\/" p2) [= q by A4, FILTER_0: 6, FILTER_0: 7;

          hence (p1 "/\" p2) in P & (p1 "\/" p2) in P by A5;

        end;

        then (for p1,p2 be Element of L st p1 in P & p2 in P holds (p1 "/\" p2) in P) & for p1,p2 be Element of L st p1 in P & p2 in P holds (p1 "\/" p2) in P;

        hence thesis by LATTICES:def 24, LATTICES:def 25;

      end;

    end

    theorem :: FILTER_2:62



     Th62: p [= q implies (r in [#p, q#] iff p [= r & r [= q)

    proof

      assume p [= q;

      then [#p, q#] = { s where s be Element of L : p [= s & s [= q } by Def12;

      then r in [#p, q#] iff ex s be Element of L st r = s & p [= s & s [= q;

      hence thesis;

    end;

    theorem :: FILTER_2:63

    p [= q implies p in [#p, q#] & q in [#p, q#] by Th62;

    theorem :: FILTER_2:64

     [#p, p#] = {p}

    proof

      let q;

      hereby

        assume q in [#p, p#];

        then p [= q & q [= p by Th62;

        then q = p by LATTICES: 8;

        hence q in {p} by TARSKI:def 1;

      end;

      p in [#p, p#] by Th62;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FILTER_2:65

    L is upper-bounded implies <.p.) = [#p, ( Top L)#]

    proof

      assume

       A1: L is upper-bounded;

      let q;



       A2: q in <.p.) iff p [= q by FILTER_0: 15;

      p [= ( Top L) & q [= ( Top L) by A1, LATTICES: 19;

      hence thesis by A2, Th62;

    end;

    theorem :: FILTER_2:66

    L is lower-bounded implies (.p.> = [#( Bottom L), p#]

    proof

      assume

       A1: L is lower-bounded;

      let q;



       A2: q in (.p.> iff q [= p by Th28;

      ( Bottom L) [= p & ( Bottom L) [= q by A1;

      hence thesis by A2, Th62;

    end;

    theorem :: FILTER_2:67

    for L1,L2 be Lattice holds for F1 be Filter of L1, F2 be Filter of L2 st the LattStr of L1 = the LattStr of L2 & F1 = F2 holds ( latt F1) = ( latt F2)

    proof

      let L1,L2 be Lattice, F1 be Filter of L1, F2 be Filter of L2;

      ex o1,o2 be BinOp of F1 st o1 = (the L_join of L1 || F1) & o2 = (the L_meet of L1 || F1) & ( latt F1) = LattStr (# F1, o1, o2 #) by FILTER_0:def 9;

      hence thesis by FILTER_0:def 9;

    end;

    begin

    notation

      let L;

      synonym Sublattice of L for SubLattice of L;

    end

    definition

      let L;

      :: original: Sublattice

      redefine

      :: FILTER_2:def13

      mode Sublattice of L means

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

      compatibility

      proof

        let K be Lattice;

        thus K is SubLattice of L implies ex P, o1, o2 st o1 = (the L_join of L || P) & o2 = (the L_meet of L || P) & the LattStr of K = LattStr (# P, o1, o2 #)

        proof

          assume

           A1: K is SubLattice of L;

          then

           A2: met(K) = ( met(L) || carr(K)) by NAT_LAT:def 12;

          reconsider P = carr(K) as non empty Subset of L by A1, NAT_LAT:def 12;



           A3: join(K) = ( join(L) || carr(K)) by A1, NAT_LAT:def 12;

          now

            let p,q be Element of L;

            assume p in P & q in P;

            then

             A4: [p, q] in [:P, P:] by ZFMISC_1: 87;

            ( dom met(K)) = [:P, P:] by FUNCT_2:def 1;

            then

             A5: ( met(L) . [p, q]) = ( met(K) . [p, q]) by A2, A4, FUNCT_1: 47;

            ( dom join(K)) = [:P, P:] by FUNCT_2:def 1;

            then ( join(L) . [p, q]) = ( join(K) . [p, q]) by A3, A4, FUNCT_1: 47;

            hence (p "/\" q) in P & (p "\/" q) in P by A4, A5, FUNCT_2: 5;

          end;

          then (for p1,p2 be Element of L st p1 in P & p2 in P holds (p1 "/\" p2) in P) & for p1,p2 be Element of L st p1 in P & p2 in P holds (p1 "\/" p2) in P;

          then

          reconsider P as non empty ClosedSubset of L by LATTICES:def 24, LATTICES:def 25;

          take P;

          reconsider o1 = join(K), o2 = met(K) as BinOp of P;

          take o1, o2;

          thus thesis by A1, NAT_LAT:def 12;

        end;

        given P, o1, o2 such that

         A6: o1 = (the L_join of L || P) & o2 = (the L_meet of L || P) & the LattStr of K = LattStr (# P, o1, o2 #);

        thus thesis by A6, NAT_LAT:def 12;

      end;

    end

    theorem :: FILTER_2:68



     Th68: for K be Sublattice of L, a be Element of K holds a is Element of L by NAT_LAT:def 12, TARSKI:def 3;

    definition

      let L, P;

      :: FILTER_2:def14

      func latt (L,P) -> Sublattice of L means

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

      existence

      proof

        reconsider o1 = ( join(L) || P), o2 = ( met(L) || P) as BinOp of P by Th60;

        o1 = ( join(L) || P);

        then

         A1: o2 is commutative associative by Th61;

        o2 = ( met(L) || P);

        then

         A2: o1 is commutative associative by Th61;

        o1 absorbs o2 & o2 absorbs o1 by Th61;

        then

        reconsider K = LattStr (# P, o1, o2 #) as strict Lattice by A2, A1, LATTICE2: 11;

        reconsider K as strict Sublattice of L by NAT_LAT:def 12;

        take K, o1, o2;

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let L, P;

      cluster ( latt (L,P)) -> strict;

      coherence

      proof

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

        hence thesis;

      end;

    end

    definition

      let L;

      let l be Sublattice of L;

      :: original: .:

      redefine

      func l .: -> strict Sublattice of (L .: ) ;

      coherence

      proof

        consider P, o1, o2 such that

         A1: o1 = ( join(L) || P) & o2 = ( met(L) || P) & the LattStr of l = LattStr (# P, o1, o2 #) by Def13;

        (l .: ) is Sublattice of (L .: )

        proof

          take (P .: );

          thus thesis by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: FILTER_2:69



     Th69: ( latt F) = ( latt (L,F))

    proof

      ex o1,o2 be BinOp of F st o1 = ( join(L) || F) & o2 = ( met(L) || F) & ( latt (L,F)) = LattStr (# F, o1, o2 #) by Def14;

      hence thesis by FILTER_0:def 9;

    end;

    theorem :: FILTER_2:70



     Th70: ( latt (L,P)) = (( latt ((L .: ),(P .: ))) .: )

    proof

      (ex o1, o2 st o1 = ( join(L) || P) & o2 = ( met(L) || P) & ( latt (L,P)) = LattStr (# P, o1, o2 #)) & ex o3,o4 be BinOp of (P .: ) st o3 = ( join(.:) || (P .: )) & o4 = ( met(.:) || (P .: )) & ( latt ((L .: ),(P .: ))) = LattStr (# (P .: ), o3, o4 #) by Def14;

      hence thesis;

    end;

    theorem :: FILTER_2:71

    ( latt (L, (.L.>)) = the LattStr of L & ( latt (L, <.L.))) = the LattStr of L

    proof



       A1: ( dom met(L)) = [: carr(L), carr(L):] & ( join(L) | ( dom join(L)) qua set) = join(L) by FUNCT_2:def 1, RELAT_1: 68;

      (ex o1,o2 be BinOp of (.L.> st o1 = (the L_join of L || (.L.>) & o2 = (the L_meet of L || (.L.>) & ( latt (L, (.L.>)) = LattStr (# (.L.>, o1, o2 #)) & ( dom join(L)) = [: carr(L), carr(L):] by Def14, FUNCT_2:def 1;

      hence thesis by A1, RELAT_1: 68;

    end;

    theorem :: FILTER_2:72



     Th72: the carrier of ( latt (L,P)) = P & the L_join of ( latt (L,P)) = (the L_join of L || P) & the L_meet of ( latt (L,P)) = (the L_meet of L || P)

    proof

      ex o1, o2 st o1 = ( join(L) || P) & o2 = ( met(L) || P) & ( latt (L,P)) = LattStr (# P, o1, o2 #) by Def14;

      hence thesis;

    end;

    theorem :: FILTER_2:73



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

    proof

      let p, q;

      let p9,q9 be Element of ( latt (L,P));

      assume

       A1: p = p9 & q = q9;

      consider o1, o2 such that

       A2: o1 = ( join(L) || P) and

       A3: o2 = ( met(L) || P) and

       A4: ( latt (L,P)) = LattStr (# P, o1, o2 #) by Def14;



       A5: [p9, q9] in [:P, P:] by A4;

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

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

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

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

    end;

    theorem :: FILTER_2:74



     Th74: for p, q holds for p9,q9 be Element of ( latt (L,P)) st p = p9 & q = q9 holds p [= q iff p9 [= q9 by Th73;

    theorem :: FILTER_2:75

    L is lower-bounded implies ( latt (L,I)) is lower-bounded

    proof

      set b9 = the Element of ( latt (L,I));

      reconsider b = b9 as Element of L by Th68;

      given c be Element of L such that

       A1: for a be Element of L holds (c "/\" a) = c & (a "/\" c) = c;



       A2: carr(latt) = I by Th72;

      (c "/\" b) = c by A1;

      then

      reconsider c9 = c as Element of ( latt (L,I)) by A2, Th22;

      take c9;

      let a9 be Element of ( latt (L,I));

      reconsider a = a9 as Element of L by Th68;



      thus (c9 "/\" a9) = (c "/\" a) by Th73

      .= c9 by A1;

      hence (a9 "/\" c9) = c9;

    end;

    theorem :: FILTER_2:76

    L is modular implies ( latt (L,P)) is modular

    proof

      assume

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

      let a9,b9,c9 be Element of ( latt (L,P));

      reconsider a = a9, b = b9, c = c9, bc = (b9 "/\" c9), ab = (a9 "\/" b9) as Element of L by Th68;

      assume a9 [= c9;

      then

       A2: a [= c by Th74;



      thus (a9 "\/" (b9 "/\" c9)) = (a "\/" bc) by Th73

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

      .= ((a "\/" b) "/\" c) by A1, A2

      .= (ab "/\" c) by Th73

      .= ((a9 "\/" b9) "/\" c9) by Th73;

    end;

    theorem :: FILTER_2:77



     Th77: L is distributive implies ( latt (L,P)) is distributive

    proof

      assume

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

      let a9,b9,c9 be Element of ( latt (L,P));

      reconsider a = a9, b = b9, c = c9, bc = (b9 "\/" c9), ab = (a9 "/\" b9), ac = (a9 "/\" c9) as Element of L by Th68;



      thus (a9 "/\" (b9 "\/" c9)) = (a "/\" bc) by Th73

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

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

      .= (ab "\/" (a "/\" c)) by Th73

      .= (ab "\/" ac) by Th73

      .= ((a9 "/\" b9) "\/" (a9 "/\" c9)) by Th73;

    end;

    theorem :: FILTER_2:78

    L is implicative & p [= q implies ( latt (L, [#p, q#])) is implicative

    proof

      assume

       A1: L is implicative;

      set P = [#p, q#], K = ( latt (L,P));

      assume

       A2: p [= q;

      let a9,b9 be Element of ( latt (L,P));

      reconsider a = a9, b = b9 as Element of L by Th68;

      set c = (a => b);



       A3: carr(K) = P by Th72;

      then p [= a by A2, Th62;

      then

       A4: (p "\/" (c "/\" a)) = ((p "\/" c) "/\" a) by A1, LATTICES:def 12;



       A5: (a "/\" c) [= b by A1, FILTER_0:def 7;

      p [= b by A2, A3, Th62;

      then (p "\/" (a "/\" c)) [= b by A5, FILTER_0: 6;

      then

       A6: ((p "\/" (a "/\" c)) "/\" q) [= b by FILTER_0: 2;

      set d = ((c "\/" p) "/\" q);

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

      then d [= q & p [= d by A2, FILTER_0: 7, LATTICES: 6;

      then

      reconsider d9 = d as Element of K by A2, A3, Th62;

      take d9;

      (((p "\/" c) "/\" a) "/\" q) = (a "/\" d) & (a "/\" d) = (a9 "/\" d9) by Th73, LATTICES:def 7;

      hence (a9 "/\" d9) [= b9 by A4, A6, Th74;

      let e9 be Element of K;

      reconsider e = e9, ae = (a9 "/\" e9) as Element of L by Th68;

      e [= q by A2, A3, Th62;

      then

       A7: e = (e "/\" q) by LATTICES: 4;

      assume (a9 "/\" e9) [= b9;

      then ae [= b by Th74;

      then (a "/\" e) [= b by Th73;

      then

       A8: e [= c by A1, FILTER_0:def 7;

      p [= e by A2, A3, Th62;

      then e = (e "\/" p);

      then e [= (c "\/" p) by A8, FILTER_0: 1;

      then e [= d by A7, LATTICES: 9;

      hence e9 [= d9 by Th74;

    end;

    registration

      let L, p;

      cluster ( latt (L, (.p.>)) -> upper-bounded;

      coherence

      proof

        ( latt (L, (.p.>)) = (( latt ((L .: ),( (.p.> .: ))) .: ) by Th70

        .= (( latt ((L .: ), <.(p .: ).))) .: ) by Th29

        .= (( latt <.(p .: ).)) .: ) by Th69;

        hence thesis by LATTICE2: 48;

      end;

    end

    theorem :: FILTER_2:79



     Th79: ( Top ( latt (L, (.p.>))) = p

    proof

      ( latt (L, (.p.>)) = (( latt ((L .: ),( (.p.> .: ))) .: ) by Th70

      .= (( latt ((L .: ), <.(p .: ).))) .: ) by Th29

      .= (( latt <.(p .: ).)) .: ) by Th69;



      hence ( Top ( latt (L, (.p.>))) = ( Bottom ( latt <.(p .: ).))) by LATTICE2: 61

      .= p by FILTER_0: 56;

    end;

    theorem :: FILTER_2:80



     Th80: L is lower-bounded implies ( latt (L, (.p.>)) is lower-bounded & ( Bottom ( latt (L, (.p.>))) = ( Bottom L)

    proof

      assume

       A1: L is lower-bounded;

      then

       A2: (L .: ) is upper-bounded by LATTICE2: 48;

      then

       A3: ( latt <.(p .: ).)) is upper-bounded by FILTER_0: 52;



       A4: ( latt (L, (.p.>)) = (( latt ((L .: ),( (.p.> .: ))) .: ) by Th70

      .= (( latt ((L .: ), <.(p .: ).))) .: ) by Th29

      .= (( latt <.(p .: ).)) .: ) by Th69;

      hence ( latt (L, (.p.>)) is lower-bounded by A3, LATTICE2: 49;

      ( Top ( latt <.(p .: ).))) = ( Top (L .: )) by A2, FILTER_0: 57;



      hence ( Bottom ( latt (L, (.p.>))) = ( Top (L .: )) by A4, A3, LATTICE2: 62

      .= ( Bottom L) by A1, LATTICE2: 61;

    end;

    theorem :: FILTER_2:81



     Th81: L is lower-bounded implies ( latt (L, (.p.>)) is bounded by Th80;

    theorem :: FILTER_2:82



     Th82: p [= q implies ( latt (L, [#p, q#])) is bounded & ( Top ( latt (L, [#p, q#]))) = q & ( Bottom ( latt (L, [#p, q#]))) = p

    proof

      assume

       A1: p [= q;



       A2: carr(latt) = [#p, q#] by Th72;

      then

      reconsider p9 = p, q9 = q as Element of ( latt (L, [#p, q#])) by A1, Th62;

       A3:

      now

        let a9 be Element of ( latt (L, [#p, q#]));

        reconsider a = a9 as Element of L by Th68;



         A4: a [= q by A1, A2, Th62;



        thus (q9 "\/" a9) = (q "\/" a) by Th73

        .= q9 by A4;

        hence (a9 "\/" q9) = q9;

      end;

       A5:

      now

        let a9 be Element of ( latt (L, [#p, q#]));

        reconsider a = a9 as Element of L by Th68;



         A6: p [= a by A1, A2, Th62;



        thus (p9 "/\" a9) = (p "/\" a) by Th73

        .= p9 by A6, LATTICES: 4;

        hence (a9 "/\" p9) = p9;

      end;

      then

       A7: ( latt (L, [#p, q#])) is lower-bounded upper-bounded Lattice by A3, LATTICES:def 13, LATTICES:def 14;

      hence ( latt (L, [#p, q#])) is bounded;

      thus thesis by A5, A3, A7, LATTICES:def 16, LATTICES:def 17;

    end;

    theorem :: FILTER_2:83

    L is C_Lattice & L is modular implies ( latt (L, (.p.>)) is C_Lattice

    proof

      assume that

       A1: L is C_Lattice and

       A2: L is modular;

      reconsider K = ( latt (L, (.p.>)) as bounded Lattice by A1, Th81;

      K is complemented

      proof

        let b9 be Element of K;

        reconsider b = b9 as Element of L by Th68;

        consider a be Element of L such that

         A3: a is_a_complement_of b by A1, LATTICES:def 19;



         A4: (a "\/" b) = ( Top L) by A3;



         A5: carr(K) = (.p.> by Th72;

        then

         A6: b [= p by Th28;

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

        then

        reconsider a9 = (p "/\" a) as Element of K by A5, Th28;

        take a9;



        thus (a9 "\/" b9) = ((p "/\" a) "\/" b) by Th73

        .= ((b "\/" a) "/\" p) by A2, A6

        .= p by A1, A4

        .= ( Top K) by Th79;

        hence (b9 "\/" a9) = ( Top K);



         A7: (a "/\" b) = ( Bottom L) by A3;



        thus (a9 "/\" b9) = ((p "/\" a) "/\" b) by Th73

        .= (p "/\" ( Bottom L)) by A7, LATTICES:def 7

        .= ( Bottom L) by A1

        .= ( Bottom K) by A1, Th80;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: FILTER_2:84



     Th84: L is C_Lattice & L is modular & p [= q implies ( latt (L, [#p, q#])) is C_Lattice

    proof

      assume that

       A1: L is C_Lattice and

       A2: L is modular and

       A3: p [= q;

      reconsider K = ( latt (L, [#p, q#])) as bounded Lattice by A3, Th82;

      K is complemented

      proof

        let b9 be Element of K;

        reconsider b = b9 as Element of L by Th68;

        consider a be Element of L such that

         A4: a is_a_complement_of b by A1, LATTICES:def 19;



         A5: (a "/\" b) = ( Bottom L) by A4;



         A6: (a "\/" b) = ( Top L) by A4;



         A7: carr(K) = [#p, q#] by Th72;

        then

         A8: b [= q by A3, Th62;

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

        then p [= (p "\/" (a "/\" q)) & (p "\/" (a "/\" q)) [= q by A3, FILTER_0: 6, LATTICES: 5;

        then

        reconsider a9 = (p "\/" (a "/\" q)) as Element of K by A3, A7, Th62;

        take a9;



         A9: p [= b by A3, A7, Th62;



        thus (a9 "\/" b9) = ((p "\/" (a "/\" q)) "\/" b) by Th73

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

        .= (b "\/" (a "/\" q)) by A9

        .= (( Top L) "/\" q) by A2, A6, A8

        .= q by A1

        .= ( Top K) by A3, Th82;

        hence (b9 "\/" a9) = ( Top K);



        thus (a9 "/\" b9) = ((p "\/" (a "/\" q)) "/\" b) by Th73

        .= (p "\/" ((a "/\" q) "/\" b)) by A2, A9

        .= (p "\/" (q "/\" ( Bottom L))) by A5, LATTICES:def 7

        .= (p "\/" ( Bottom L)) by A1

        .= p by A1

        .= ( Bottom K) by A3, Th82;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: FILTER_2:85

    L is B_Lattice & p [= q implies ( latt (L, [#p, q#])) is B_Lattice

    proof

      assume L is B_Lattice & p [= q;

      then ( latt (L, [#p, q#])) is bounded complemented distributive Lattice by Th77, Th84;

      hence thesis;

    end;

    theorem :: FILTER_2:86

    for S be non empty Subset of L holds S is Ideal of L iff for p,q be Element of L holds p in S & q in S iff (p "\/" q) in S by Lm1;