lattices.miz



    begin

    definition

      struct ( 1-sorted) /\-SemiLattStr (# the carrier -> set,

the L_meet -> BinOp of the carrier #)

       attr strict strict;

    end

    definition

      struct ( 1-sorted) \/-SemiLattStr (# the carrier -> set,

the L_join -> BinOp of the carrier #)

       attr strict strict;

    end

    definition

      struct ( /\-SemiLattStr, \/-SemiLattStr) LattStr (# the carrier -> set,

the L_join, L_meet -> BinOp of the carrier #)

       attr strict strict;

    end

    registration

      let D be non empty set, u be BinOp of D;

      cluster \/-SemiLattStr (# D, u #) -> non empty;

      coherence ;

      cluster /\-SemiLattStr (# D, u #) -> non empty;

      coherence ;

    end

    registration

      let D be non empty set, u,n be BinOp of D;

      cluster LattStr (# D, u, n #) -> non empty;

      coherence ;

    end

    registration

      cluster 1 -element strict for \/-SemiLattStr;

      existence

      proof

        set u = the BinOp of ( bool {} );

        take L = \/-SemiLattStr (# ( bool {} ), u #);

        thus thesis by ZFMISC_1: 1;

      end;

      cluster 1 -element strict for /\-SemiLattStr;

      existence

      proof

        set u = the BinOp of ( bool {} );

        take L = /\-SemiLattStr (# ( bool {} ), u #);

        thus thesis by ZFMISC_1: 1;

      end;

      cluster 1 -element strict for LattStr;

      existence

      proof

        set u = the BinOp of ( bool {} );

        take L = LattStr (# ( bool {} ), u, u #);

        thus thesis by ZFMISC_1: 1;

      end;

    end

    definition

      let G be non empty \/-SemiLattStr, p,q be Element of G;

      :: LATTICES:def1

      func p "\/" q -> Element of G equals (the L_join of G . (p,q));

      coherence ;

    end

    definition

      let G be non empty /\-SemiLattStr, p,q be Element of G;

      :: LATTICES:def2

      func p "/\" q -> Element of G equals (the L_meet of G . (p,q));

      coherence ;

    end

    definition

      let G be non empty \/-SemiLattStr, p,q be Element of G;

      :: LATTICES:def3

      pred p [= q means

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

    end

    

     Lm1: for uu,nn be BinOp of ( bool {} ), x,y be Element of LattStr (# ( bool {} ), uu, nn #) holds x = y

    proof

      let uu,nn be BinOp of ( bool {} ), x,y be Element of LattStr (# ( bool {} ), uu, nn #);

      x = {} ;

      hence thesis;

    end;

    

     Lm2: for n be BinOp of ( bool {} ), x,y be Element of \/-SemiLattStr (# ( bool {} ), n #) holds x = y

    proof

      let n be BinOp of ( bool {} );

      let x,y be Element of \/-SemiLattStr (# ( bool {} ), n #);

      x = {} ;

      hence thesis;

    end;

    

     Lm3: for n be BinOp of ( bool {} ), x,y be Element of /\-SemiLattStr (# ( bool {} ), n #) holds x = y

    proof

      let n be BinOp of ( bool {} );

      let x,y be Element of /\-SemiLattStr (# ( bool {} ), n #);

      x = {} ;

      hence thesis;

    end;

    definition

      let IT be non empty \/-SemiLattStr;

      :: LATTICES:def4

      attr IT is join-commutative means

      : Def4: for a,b be Element of IT holds (a "\/" b) = (b "\/" a);

      :: LATTICES:def5

      attr IT is join-associative means

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

    end

    definition

      let IT be non empty /\-SemiLattStr;

      :: LATTICES:def6

      attr IT is meet-commutative means

      : Def6: for a,b be Element of IT holds (a "/\" b) = (b "/\" a);

      :: LATTICES:def7

      attr IT is meet-associative means

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

    end

    definition

      let IT be non empty LattStr;

      :: LATTICES:def8

      attr IT is meet-absorbing means

      : Def8: for a,b be Element of IT holds ((a "/\" b) "\/" b) = b;

      :: LATTICES:def9

      attr IT is join-absorbing means

      : Def9: for a,b be Element of IT holds (a "/\" (a "\/" b)) = a;

    end

    definition

      let IT be non empty LattStr;

      :: LATTICES:def10

      attr IT is Lattice-like means IT is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing;

    end

    registration

      cluster Lattice-like -> join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing for non empty LattStr;

      coherence ;

      cluster join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing -> Lattice-like for non empty LattStr;

      coherence ;

    end

    registration

      cluster strict join-commutative join-associative for non empty \/-SemiLattStr;

      existence

      proof

        set u = the BinOp of ( bool {} );

        take GGj = \/-SemiLattStr (# ( bool {} ), u #);

        (for x,y be Element of GGj holds (x "\/" y) = (y "\/" x)) & for x,y,z be Element of GGj holds (x "\/" (y "\/" z)) = ((x "\/" y) "\/" z) by Lm2;

        hence thesis;

      end;

      cluster strict meet-commutative meet-associative for non empty /\-SemiLattStr;

      existence

      proof

        set u = the BinOp of ( bool {} );

        take GGm = /\-SemiLattStr (# ( bool {} ), u #);

        (for x,y be Element of GGm holds (x "/\" y) = (y "/\" x)) & for x,y,z be Element of GGm holds (x "/\" (y "/\" z)) = ((x "/\" y) "/\" z) by Lm3;

        hence thesis;

      end;

      cluster strict Lattice-like for non empty LattStr;

      existence

      proof

        set u = the BinOp of ( bool {} );

        take GG = LattStr (# ( bool {} ), u, u #);

        

         A1: (for x,y be Element of GG holds ((x "/\" y) "\/" y) = y) & for x,y be Element of GG holds (x "/\" y) = (y "/\" x) by Lm1;

        

         A2: (for x,y,z be Element of GG holds (x "/\" (y "/\" z)) = ((x "/\" y) "/\" z)) & for x,y be Element of GG holds (x "/\" (x "\/" y)) = x by Lm1;

        (for x,y be Element of GG holds (x "\/" y) = (y "\/" x)) & for x,y,z be Element of GG holds (x "\/" (y "\/" z)) = ((x "\/" y) "\/" z) by Lm1;

        then GG is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1, A2;

        hence thesis;

      end;

    end

    definition

      mode Lattice is Lattice-like non empty LattStr;

    end

    definition

      let L be join-commutative non empty \/-SemiLattStr, a,b be Element of L;

      :: original: "\/"

      redefine

      func a "\/" b;

      commutativity by Def4;

    end

    definition

      let L be meet-commutative non empty /\-SemiLattStr, a,b be Element of L;

      :: original: "/\"

      redefine

      func a "/\" b;

      commutativity by Def6;

    end

    definition

      let IT be non empty LattStr;

      :: LATTICES:def11

      attr IT is distributive means

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

    end

    definition

      let IT be non empty LattStr;

      :: LATTICES:def12

      attr IT is modular means for a,b,c be Element of IT st a [= c holds (a "\/" (b "/\" c)) = ((a "\/" b) "/\" c);

    end

    definition

      let IT be non empty /\-SemiLattStr;

      :: LATTICES:def13

      attr IT is lower-bounded means

      : Def13: ex c be Element of IT st for a be Element of IT holds (c "/\" a) = c & (a "/\" c) = c;

    end

    definition

      let IT be non empty \/-SemiLattStr;

      :: LATTICES:def14

      attr IT is upper-bounded means

      : Def14: ex c be Element of IT st for a be Element of IT holds (c "\/" a) = c & (a "\/" c) = c;

    end

    

     Lm4: for n,u be BinOp of ( bool {} ) holds LattStr (# ( bool {} ), n, u #) is Lattice

    proof

      let n,u be BinOp of ( bool {} );

      set G = LattStr (# ( bool {} ), n, u #);

      for x,y,z be Element of G holds (x "\/" (y "\/" z)) = ((x "\/" y) "\/" z) by Lm1;

      then

       A1: G is join-associative;

      for x,y be Element of G holds ((x "/\" y) "\/" y) = y by Lm1;

      then

       A2: G is meet-absorbing;

      for x,y be Element of G holds (x "/\" (x "\/" y)) = x by Lm1;

      then

       A3: G is join-absorbing;

      for x,y,z be Element of G holds (x "/\" (y "/\" z)) = ((x "/\" y) "/\" z) by Lm1;

      then

       A4: G is meet-associative;

      for x,y be Element of G holds (x "/\" y) = (y "/\" x) by Lm1;

      then

       A5: G is meet-commutative;

      for x,y be Element of G holds (x "\/" y) = (y "\/" x) by Lm1;

      then G is join-commutative;

      hence thesis by A1, A2, A5, A4, A3;

    end;

    registration

      cluster strict distributive lower-bounded upper-bounded modular for Lattice;

      existence

      proof

        set uu = the BinOp of ( bool {} );

        set GG = LattStr (# ( bool {} ), uu, uu #);

        reconsider GG as Lattice by Lm4;

        reconsider 0GG = {} , D = {} as Element of GG by ZFMISC_1:def 1;

        for x be Element of GG holds (0GG "/\" x) = 0GG & (x "/\" 0GG) = 0GG;

        then

         A1: GG is lower-bounded;

        for x be Element of GG holds (D "\/" x) = D & (x "\/" D) = D;

        then

         A2: GG is upper-bounded;

        for x,y,z be Element of GG holds (x "/\" (y "\/" z)) = ((x "/\" y) "\/" (x "/\" z)) by Lm1;

        then

         A3: GG is distributive;

        for x,y,z be Element of GG holds x [= z implies (x "\/" (y "/\" z)) = ((x "\/" y) "/\" z) by Lm1;

        then GG is modular;

        hence thesis by A1, A3, A2;

      end;

    end

    definition

      mode D_Lattice is distributive Lattice;

      mode M_Lattice is modular Lattice;

      mode 0_Lattice is lower-bounded Lattice;

      mode 1_Lattice is upper-bounded Lattice;

    end

    

     Lm5: for n,u be BinOp of ( bool {} ) holds LattStr (# ( bool {} ), n, u #) is 0_Lattice

    proof

      let n,u be BinOp of ( bool {} );

      set G = LattStr (# ( bool {} ), n, u #);

      reconsider G as Lattice by Lm4;

      reconsider D = {} as Element of G by ZFMISC_1:def 1;

      for x be Element of G holds (D "/\" x) = D & (x "/\" D) = D;

      hence thesis by Def13;

    end;

    

     Lm6: for n,u be BinOp of ( bool {} ) holds LattStr (# ( bool {} ), n, u #) is 1_Lattice

    proof

      let n,u be BinOp of ( bool {} );

      set G = LattStr (# ( bool {} ), n, u #);

      reconsider G as Lattice by Lm4;

      reconsider D = {} as Element of G by ZFMISC_1:def 1;

      for x be Element of G holds (D "\/" x) = D & (x "\/" D) = D;

      hence thesis by Def14;

    end;

    definition

      let IT be non empty LattStr;

      :: LATTICES:def15

      attr IT is bounded means IT is lower-bounded upper-bounded;

    end

    registration

      cluster lower-bounded upper-bounded -> bounded for non empty LattStr;

      coherence ;

      cluster bounded -> lower-bounded upper-bounded for non empty LattStr;

      coherence ;

    end

    registration

      cluster bounded strict for Lattice;

      existence

      proof

        set uu = the BinOp of ( bool {} );

        set G = LattStr (# ( bool {} ), uu, uu #);

        reconsider G as Lattice by Lm4;

        G is 0_Lattice & G is 1_Lattice by Lm5, Lm6;

        hence thesis;

      end;

    end

    definition

      mode 01_Lattice is bounded Lattice;

    end

    definition

      let L be non empty /\-SemiLattStr;

      assume

       A1: L is lower-bounded;

      :: LATTICES:def16

      func Bottom L -> Element of L means

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

      existence by A1;

      uniqueness

      proof

        let c1,c2 be Element of L such that

         A2: for a be Element of L holds (c1 "/\" a) = c1 & (a "/\" c1) = c1 and

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

        

        thus c1 = (c2 "/\" c1) by A2

        .= c2 by A3;

      end;

    end

    definition

      let L be non empty \/-SemiLattStr;

      assume

       A1: L is upper-bounded;

      :: LATTICES:def17

      func Top L -> Element of L means

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

      existence by A1;

      uniqueness

      proof

        let c1,c2 be Element of L such that

         A2: for a be Element of L holds (c1 "\/" a) = c1 & (a "\/" c1) = c1 and

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

        

        thus c1 = (c2 "\/" c1) by A2

        .= c2 by A3;

      end;

    end

    definition

      let L be non empty LattStr, a,b be Element of L;

      :: LATTICES:def18

      pred a is_a_complement_of b means (a "\/" b) = ( Top L) & (b "\/" a) = ( Top L) & (a "/\" b) = ( Bottom L) & (b "/\" a) = ( Bottom L);

    end

    definition

      let IT be non empty LattStr;

      :: LATTICES:def19

      attr IT is complemented means

      : Def19: for b be Element of IT holds ex a be Element of IT st a is_a_complement_of b;

    end

    registration

      cluster bounded complemented strict for Lattice;

      existence

      proof

        set n = the BinOp of ( bool {} );

        reconsider GG = LattStr (# ( bool {} ), n, n #) as strict Lattice by Lm4;

        take GG;

        GG is 0_Lattice & GG is 1_Lattice by Lm5, Lm6;

        hence GG is bounded;

        thus GG is complemented

        proof

          set a = the Element of GG;

          let b be Element of GG;

          take a;

          thus (a "\/" b) = ( Top GG) & (b "\/" a) = ( Top GG) by Lm1;

          thus (a "/\" b) = ( Bottom GG) & (b "/\" a) = ( Bottom GG) by Lm1;

        end;

        thus thesis;

      end;

    end

    definition

      mode C_Lattice is complemented 01_Lattice;

    end

    definition

      let IT be non empty LattStr;

      :: LATTICES:def20

      attr IT is Boolean means IT is bounded complemented distributive;

    end

    registration

      cluster Boolean -> bounded complemented distributive for non empty LattStr;

      coherence ;

      cluster bounded complemented distributive -> Boolean for non empty LattStr;

      coherence ;

    end

    registration

      cluster Boolean strict for Lattice;

      existence

      proof

        set n = the BinOp of ( bool {} );

        reconsider G = LattStr (# ( bool {} ), n, n #) as strict Lattice by Lm4;

        

         A1: G is complemented

        proof

          let b be Element of G;

          take b;

          thus (b "\/" b) = ( Top G) & (b "\/" b) = ( Top G) by Lm1;

          thus (b "/\" b) = ( Bottom G) & (b "/\" b) = ( Bottom G) by Lm1;

        end;

        G is 0_Lattice & G is 1_Lattice by Lm5, Lm6;

        then

        reconsider G as C_Lattice by A1;

        for x,y,z be Element of G holds (x "/\" (y "\/" z)) = ((x "/\" y) "\/" (x "/\" z)) by Lm1;

        then G is distributive;

        hence thesis;

      end;

    end

    definition

      mode B_Lattice is Boolean Lattice;

    end

    registration

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

      reduce (a "\/" a) to a;

      reducibility

      proof

        

        thus (a "\/" a) = ((a "/\" (a "\/" a)) "\/" a) by Def9

        .= a by Def8;

      end;

    end

    registration

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

      reduce (a "/\" a) to a;

      reducibility

      proof

        (a "/\" (a "\/" a)) = a by Def9;

        hence thesis;

      end;

    end

    ::$Canceled

    theorem :: LATTICES:3

    

     Th1: for L be Lattice holds (for a,b,c be Element of L holds (a "/\" (b "\/" c)) = ((a "/\" b) "\/" (a "/\" c))) iff for a,b,c be Element of L holds (a "\/" (b "/\" c)) = ((a "\/" b) "/\" (a "\/" c))

    proof

      let L be Lattice;

      hereby

        assume

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

        let a,b,c be Element of L;

        

        thus (a "\/" (b "/\" c)) = ((a "\/" (c "/\" a)) "\/" (c "/\" b)) by Def8

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

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

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

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

      end;

      assume

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

      let a,b,c be Element of L;

      

      thus (a "/\" (b "\/" c)) = ((a "/\" (c "\/" a)) "/\" (c "\/" b)) by Def9

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

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

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

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

    end;

    theorem :: LATTICES:4

    

     Th2: for L be meet-absorbing join-absorbing non empty LattStr, a,b be Element of L holds a [= b iff (a "/\" b) = a by Def8, Def9;

    theorem :: LATTICES:5

    

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

    proof

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

      

      thus (a "\/" (a "\/" b)) = ((a "\/" a) "\/" b) by Def5

      .= (a "\/" b);

    end;

    theorem :: LATTICES:6

    

     Th4: for L be meet-absorbing meet-commutative non empty LattStr, a,b be Element of L holds (a "/\" b) [= a by Def8;

    definition

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

      :: original: [=

      redefine

      pred a [= b;

      reflexivity ;

    end

    theorem :: LATTICES:7

    for L be join-associative non empty \/-SemiLattStr, a,b,c be Element of L holds a [= b & b [= c implies a [= c by Def5;

    theorem :: LATTICES:8

    

     Th6: for L be join-commutative non empty \/-SemiLattStr, a,b be Element of L holds a [= b & b [= a implies a = b

    proof

      let L be join-commutative non empty \/-SemiLattStr, a,b be Element of L;

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

      hence thesis;

    end;

    theorem :: LATTICES:9

    

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

    proof

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

      assume a [= b;

      

      hence ((a "/\" c) "\/" (b "/\" c)) = (((a "/\" b) "/\" c) "\/" (b "/\" c)) by Th2

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

      .= (b "/\" c) by Def8;

    end;

    theorem :: LATTICES:10

    for L be Lattice holds (for a,b,c be Element of L holds (((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a)) = (((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a))) implies L is distributive

    proof

      let L be Lattice;

      assume

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

       A2:

      now

        let a,b,c be Element of L;

        assume

         A3: c [= a;

        

        thus (a "/\" (b "\/" c)) = ((b "\/" c) "/\" (a "/\" (a "\/" b))) by Def9

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

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

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

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

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

        .= ((a "/\" b) "\/" ((b "/\" c) "\/" c)) by A3, Th2

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

      end;

      let a,b,c be Element of L;

      

       A4: (((a "/\" b) "\/" (c "/\" a)) "\/" a) = ((a "/\" b) "\/" ((c "/\" a) "\/" a)) by Def5

      .= ((a "/\" b) "\/" a) by Def8

      .= a by Def8;

      

      thus (a "/\" (b "\/" c)) = ((a "/\" (c "\/" a)) "/\" (b "\/" c)) by Def9

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

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

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

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

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

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

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

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

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

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

    end;

    reserve L for D_Lattice;

    reserve a,b,c for Element of L;

    theorem :: LATTICES:11

    

     Th9: (a "\/" (b "/\" c)) = ((a "\/" b) "/\" (a "\/" c))

    proof

      for a, b, c holds (a "/\" (b "\/" c)) = ((a "/\" b) "\/" (a "/\" c)) by Def11;

      hence thesis by Th1;

    end;

    theorem :: LATTICES:12

    

     Th10: (c "/\" a) = (c "/\" b) & (c "\/" a) = (c "\/" b) implies a = b

    proof

      assume that

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

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

      

      thus a = (a "/\" (c "\/" a)) by Def9

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

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

      .= b by A2, Def9;

    end;

    theorem :: LATTICES:13

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

    proof

      

      thus (((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a)) = ((((a "\/" b) "/\" (b "\/" c)) "/\" c) "\/" (((a "\/" b) "/\" (b "\/" c)) "/\" a)) by Def11

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

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

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

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

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

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

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

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

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

    end;

    registration

      cluster distributive -> modular for Lattice;

      coherence

      proof

        let L be Lattice;

        assume

         A1: L is distributive;

        let a,b,c be Element of L;

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

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

      end;

    end

    registration

      let L be 0_Lattice, a be Element of L;

      reduce (( Bottom L) "\/" a) to a;

      reducibility

      proof

        

        thus (( Bottom L) "\/" a) = ((( Bottom L) "/\" a) "\/" a) by Def16

        .= a by Def8;

      end;

      reduce (( Bottom L) "/\" a) to ( Bottom L);

      reducibility by Def16;

    end

    theorem :: LATTICES:14

    for L be 0_Lattice, a be Element of L holds (( Bottom L) "\/" a) = a;

    theorem :: LATTICES:15

    for L be 0_Lattice, a be Element of L holds (( Bottom L) "/\" a) = ( Bottom L);

    theorem :: LATTICES:16

    for L be 0_Lattice, a be Element of L holds ( Bottom L) [= a;

    registration

      let L be 1_Lattice, a be Element of L;

      reduce (( Top L) "/\" a) to a;

      reducibility

      proof

        

        thus (( Top L) "/\" a) = ((( Top L) "\/" a) "/\" a) by Def17

        .= a by Def9;

      end;

      reduce (( Top L) "\/" a) to ( Top L);

      reducibility by Def17;

    end

    theorem :: LATTICES:17

    for L be 1_Lattice, a be Element of L holds (( Top L) "/\" a) = a;

    theorem :: LATTICES:18

    for L be 1_Lattice, a be Element of L holds (( Top L) "\/" a) = ( Top L);

    theorem :: LATTICES:19

    for L be 1_Lattice, a be Element of L holds a [= ( Top L)

    proof

      let L be 1_Lattice, a be Element of L;

      (( Top L) "/\" a) [= ( Top L) by Th4;

      hence thesis;

    end;

    definition

      let L be non empty LattStr, x be Element of L;

      assume

       A1: L is complemented D_Lattice;

      :: LATTICES:def21

      func x ` -> Element of L means

      : Def21: it is_a_complement_of x;

      existence by A1, Def19;

      uniqueness by A1, Th10;

    end

    reserve L for B_Lattice;

    reserve a,b for Element of L;

    theorem :: LATTICES:20

    

     Th18: ((a ` ) "/\" a) = ( Bottom L)

    proof

      (a ` ) is_a_complement_of a by Def21;

      hence thesis;

    end;

    theorem :: LATTICES:21

    

     Th19: ((a ` ) "\/" a) = ( Top L)

    proof

      (a ` ) is_a_complement_of a by Def21;

      hence thesis;

    end;

    registration

      let L, a;

      reduce ((a ` ) ` ) to a;

      reducibility

      proof

        (a ` ) is_a_complement_of a by Def21;

        then

         A1: (a "\/" (a ` )) = ( Top L) & (a "/\" (a ` )) = ( Bottom L);

        ((a ` ) ` ) is_a_complement_of (a ` ) by Def21;

        then (((a ` ) ` ) "\/" (a ` )) = ( Top L) & (((a ` ) ` ) "/\" (a ` )) = ( Bottom L);

        hence thesis by A1, Th10;

      end;

    end

    theorem :: LATTICES:22

    ((a ` ) ` ) = a;

    theorem :: LATTICES:23

    

     Th21: ((a "/\" b) ` ) = ((a ` ) "\/" (b ` ))

    proof

      

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

      

       A2: (((a ` ) "\/" (b ` )) "/\" (a "/\" b)) = ((((a ` ) "\/" (b ` )) "/\" a) "/\" b) by Def7

      .= ((((a ` ) "/\" a) "\/" ((b ` ) "/\" a)) "/\" b) by Def11

      .= ((( Bottom L) "\/" ((b ` ) "/\" a)) "/\" b) by Th18

      .= ((b "/\" (b ` )) "/\" a) by Def7

      .= (( Bottom L) "/\" a) by Th18

      .= ( Bottom L);

      (((a ` ) "\/" (b ` )) "\/" (a "/\" b)) = ((a ` ) "\/" ((b ` ) "\/" (a "/\" b))) by Def5

      .= ((a ` ) "\/" (((b ` ) "\/" a) "/\" ((b ` ) "\/" b))) by Th9

      .= ((a ` ) "\/" (((b ` ) "\/" a) "/\" ( Top L))) by Th19

      .= ((b ` ) "\/" (a "\/" (a ` ))) by Def5

      .= ((b ` ) "\/" ( Top L)) by Th19

      .= ( Top L);

      then ((a ` ) "\/" (b ` )) is_a_complement_of (a "/\" b) by A1, A2;

      hence thesis by Def21;

    end;

    theorem :: LATTICES:24

    ((a "\/" b) ` ) = ((a ` ) "/\" (b ` ))

    proof

      

      thus ((a "\/" b) ` ) = ((((a ` ) ` ) "\/" ((b ` ) ` )) ` )

      .= ((((a ` ) "/\" (b ` )) ` ) ` ) by Th21

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

    end;

    theorem :: LATTICES:25

    

     Th23: (b "/\" a) = ( Bottom L) iff b [= (a ` )

    proof

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

      proof

        assume

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

        b = (b "/\" ( Top L))

        .= (b "/\" (a "\/" (a ` ))) by Th19

        .= (( Bottom L) "\/" (b "/\" (a ` ))) by A1, Def11

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

        then (b "\/" (a ` )) = (a ` ) by Def8;

        hence thesis;

      end;

      thus thesis

      proof

        assume b [= (a ` );

        then (b "/\" a) [= ((a ` ) "/\" a) by Th7;

        then

         A2: (b "/\" a) [= ( Bottom L) by Th18;

        ( Bottom L) [= (b "/\" a);

        hence thesis by A2, Th6;

      end;

    end;

    theorem :: LATTICES:26

    a [= b implies (b ` ) [= (a ` )

    proof

      assume a [= b;

      then ((b ` ) "/\" a) [= ((b ` ) "/\" b) by Th7;

      then

       A1: ((b ` ) "/\" a) [= ( Bottom L) by Th18;

      ( Bottom L) [= ((b ` ) "/\" a);

      then ((b ` ) "/\" a) = ( Bottom L) by A1, Th6;

      hence thesis by Th23;

    end;

    begin

    definition

      let L be non empty LattStr, S be Subset of L;

      :: LATTICES:def22

      attr S is initial means

      : Def22: for p,q be Element of L st p [= q & q in S holds p in S;

      :: LATTICES:def23

      attr S is final means

      : Def23: for p,q be Element of L st p [= q & p in S holds q in S;

      :: LATTICES:def24

      attr S is meet-closed means for p,q be Element of L st p in S & q in S holds (p "/\" q) in S;

      :: LATTICES:def25

      attr S is join-closed means for p,q be Element of L st p in S & q in S holds (p "\/" q) in S;

    end

    registration

      let L be non empty LattStr;

      cluster ( [#] L) -> initial final non empty;

      coherence ;

    end

    registration

      let L be non empty LattStr;

      cluster initial final non empty for Subset of L;

      existence

      proof

        take ( [#] L);

        thus thesis;

      end;

      cluster empty -> initial final for Subset of L;

      coherence ;

    end

    registration

      let L be Lattice;

      cluster initial final non empty for Subset of L;

      existence

      proof

        take ( [#] L);

        thus thesis;

      end;

    end

    registration

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

      cluster initial -> meet-closed for Subset of L;

      coherence by Th4;

    end

    registration

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

      cluster final -> join-closed for Subset of L;

      coherence by Th3;

    end

    theorem :: LATTICES:27

    for L be Lattice, S be initial final non empty Subset of L holds S = ( [#] L)

    proof

      let L be Lattice, S be initial final non empty Subset of L;

      consider p be Element of L such that

       A1: p in S by SUBSET_1: 4;

      for x be Element of L holds x in S iff x in ( [#] L)

      proof

        let x be Element of L;

        thus x in S implies x in ( [#] L);

        assume x in ( [#] L);

        

         A2: (x "/\" p) in S by A1, Def22, Th4;

        thus x in S by A2, Def23, Th4;

      end;

      hence S = ( [#] L) by SUBSET_1: 3;

    end;