robbins1.miz



    begin

    definition

      struct ( 1-sorted) ComplStr (# the carrier -> set,

the Compl -> UnOp of the carrier #)

       attr strict strict;

    end

    definition

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

the L_join -> BinOp of the carrier,

the Compl -> UnOp of the carrier #)

       attr strict strict;

    end

    definition

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

the L_meet -> BinOp of the carrier,

the Compl -> UnOp of the carrier #)

       attr strict strict;

    end

    definition

      struct ( ComplLLattStr, LattStr) OrthoLattStr (# the carrier -> set,

the L_join, L_meet -> BinOp of the carrier,

the Compl -> UnOp of the carrier #)

       attr strict strict;

    end

    definition

      :: ROBBINS1:def1

      func TrivComplLat -> strict ComplLLattStr equals ComplLLattStr (# { 0 }, op2 , op1 #);

      coherence ;

    end

    definition

      :: ROBBINS1:def2

      func TrivOrtLat -> strict OrthoLattStr equals OrthoLattStr (# { 0 }, op2 , op2 , op1 #);

      coherence ;

    end

    registration

      cluster TrivComplLat -> 1 -element;

      coherence ;

      cluster TrivOrtLat -> 1 -element;

      coherence ;

    end

    registration

      cluster strict1 -element for OrthoLattStr;

      existence

      proof

        take TrivOrtLat ;

        thus thesis;

      end;

      cluster strict1 -element for ComplLLattStr;

      existence

      proof

        take TrivComplLat ;

        thus thesis;

      end;

    end

    registration

      let L be 1 -element ComplLLattStr;

      cluster the ComplStr of L -> 1 -element;

      coherence ;

    end

    registration

      cluster strict1 -element for ComplStr;

      existence

      proof

        take the ComplStr of TrivOrtLat ;

        thus thesis;

      end;

    end

    definition

      let L be non empty ComplStr;

      let x be Element of L;

      :: ROBBINS1:def3

      func x ` -> Element of L equals (the Compl of L . x);

      coherence ;

    end

    notation

      let L be non empty ComplLLattStr, x,y be Element of L;

      synonym x + y for x "\/" y;

    end

    definition

      let L be non empty ComplLLattStr;

      let x,y be Element of L;

      :: ROBBINS1:def4

      func x *' y -> Element of L equals (((x ` ) "\/" (y ` )) ` );

      coherence ;

    end

    definition

      let L be non empty ComplLLattStr;

      :: ROBBINS1:def5

      attr L is Robbins means

      : Def5: for x,y be Element of L holds ((((x + y) ` ) + ((x + (y ` )) ` )) ` ) = x;

      :: ROBBINS1:def6

      attr L is Huntington means

      : Def6: for x,y be Element of L holds ((((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` )) = x;

    end

    definition

      let G be non empty \/-SemiLattStr;

      :: ROBBINS1:def7

      attr G is join-idempotent means

      : Def7: for x be Element of G holds (x "\/" x) = x;

    end

    registration

      cluster TrivComplLat -> join-commutative join-associative Robbins Huntington join-idempotent;

      coherence by STRUCT_0:def 10;

      cluster TrivOrtLat -> join-commutative join-associative Huntington Robbins;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster TrivOrtLat -> meet-commutative meet-associative meet-absorbing join-absorbing;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster strict join-associative join-commutative Robbins join-idempotent Huntington for non empty ComplLLattStr;

      existence

      proof

        take TrivComplLat ;

        thus thesis;

      end;

    end

    registration

      cluster strict Lattice-like Robbins Huntington for non empty OrthoLattStr;

      existence

      proof

        take TrivOrtLat ;

        thus thesis;

      end;

    end

    definition

      let L be join-commutative non empty ComplLLattStr, x,y be Element of L;

      :: original: +

      redefine

      func x + y;

      commutativity by LATTICES:def 4;

    end

    theorem :: ROBBINS1:1

    

     Th1: for L be Huntington join-commutative join-associative non empty ComplLLattStr, a,b be Element of L holds ((a *' b) + (a *' (b ` ))) = a by Def6;

    theorem :: ROBBINS1:2

    

     Th2: for L be Huntington join-commutative join-associative non empty ComplLLattStr, a be Element of L holds (a + (a ` )) = ((a ` ) + ((a ` ) ` ))

    proof

      let L be Huntington join-commutative join-associative non empty ComplLLattStr, a be Element of L;

      set y = (a ` ), z = ((y ` ) ` );

      a = ((((a ` ) + ((y ` ) ` )) ` ) + (((a ` ) + (y ` )) ` )) & (a ` ) = (((((a ` ) ` ) + (((a ` ) ` ) ` )) ` ) + ((((a ` ) ` ) + ((a ` ) ` )) ` )) by Def6;

      

      then (a + (a ` )) = (((((y + z) ` ) + ((y + (y ` )) ` )) + (((y ` ) + (y ` )) ` )) + (((y ` ) + z) ` )) by LATTICES:def 5

      .= ((((((y ` ) + (y ` )) ` ) + ((y + (y ` )) ` )) + ((y + z) ` )) + (((y ` ) + z) ` )) by LATTICES:def 5

      .= (((((y ` ) + y) ` ) + (((y ` ) + (y ` )) ` )) + (((y + z) ` ) + (((y ` ) + z) ` ))) by LATTICES:def 5

      .= (y + (((y + z) ` ) + (((y ` ) + z) ` ))) by Def6

      .= (y + (y ` )) by Def6;

      hence thesis;

    end;

    theorem :: ROBBINS1:3

    

     Th3: for L be join-commutative join-associative Huntington non empty ComplLLattStr, x be Element of L holds ((x ` ) ` ) = x

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, x be Element of L;

      set y = (x ` );

      (((((y ` ) ` ) + (y ` )) ` ) + ((((y ` ) ` ) + y) ` )) = (y ` ) & (((y + ((y ` ) ` )) ` ) + ((y + (y ` )) ` )) = x by Def6;

      hence thesis by Th2;

    end;

    theorem :: ROBBINS1:4

    

     Th4: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L holds (a + (a ` )) = (b + (b ` ))

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L;

      

      thus (a + (a ` )) = (((((a ` ) + ((b ` ) ` )) ` ) + (((a ` ) + (b ` )) ` )) + (a ` )) by Def6

      .= (((((a ` ) + ((b ` ) ` )) ` ) + (((a ` ) + (b ` )) ` )) + (((((a ` ) ` ) + ((b ` ) ` )) ` ) + ((((a ` ) ` ) + (b ` )) ` ))) by Def6

      .= (((((a ` ) ` ) + (b ` )) ` ) + (((((a ` ) ` ) + ((b ` ) ` )) ` ) + ((((a ` ) + ((b ` ) ` )) ` ) + (((a ` ) + (b ` )) ` )))) by LATTICES:def 5

      .= (((((a ` ) ` ) + (b ` )) ` ) + ((((a ` ) + (b ` )) ` ) + ((((a ` ) + ((b ` ) ` )) ` ) + ((((a ` ) ` ) + ((b ` ) ` )) ` )))) by LATTICES:def 5

      .= ((((((a ` ) ` ) + (b ` )) ` ) + (((a ` ) + (b ` )) ` )) + ((((a ` ) + ((b ` ) ` )) ` ) + ((((a ` ) ` ) + ((b ` ) ` )) ` ))) by LATTICES:def 5

      .= (b + (((((a ` ) ` ) + ((b ` ) ` )) ` ) + (((a ` ) + ((b ` ) ` )) ` ))) by Def6

      .= (b + (b ` )) by Def6;

    end;

    theorem :: ROBBINS1:5

    

     Th5: for L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr holds ex c be Element of L st for a be Element of L holds (c + a) = c & (a + (a ` )) = c

    proof

      let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr;

      set b = the Element of L;

      take c = ((b ` ) + b);

      let a be Element of L;

      

      thus (c + a) = (((a ` ) + a) + a) by Th4

      .= ((a ` ) + (a + a)) by LATTICES:def 5

      .= ((a ` ) + a) by Def7

      .= c by Th4;

      thus thesis by Th4;

    end;

    theorem :: ROBBINS1:6

    

     Th6: for L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr holds L is upper-bounded

    proof

      let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr;

      consider c be Element of L such that

       A1: for a be Element of L holds (c + a) = c & (a + (a ` )) = c by Th5;

      for a be Element of L holds (a + c) = c & (a + (a ` )) = c by A1;

      hence thesis by A1;

    end;

    registration

      cluster join-commutative join-associative join-idempotent Huntington -> upper-bounded for non empty ComplLLattStr;

      coherence by Th6;

    end

    definition

      let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr;

      :: original: Top

      redefine

      :: ROBBINS1:def8

      func Top L means

      : Def8: ex a be Element of L st it = (a + (a ` ));

      compatibility

      proof

        let IT be Element of L;

        hereby

          set a = the Element of L;

          assume

           A1: IT = ( Top L);

          take a;

          for b be Element of L holds ((a + (a ` )) + b) = (a + (a ` )) & (b + (a + (a ` ))) = (a + (a ` ))

          proof

            let b be Element of L;

            ((a + (a ` )) + b) = ((b + (b ` )) + b) by Th4

            .= ((b ` ) + (b + b)) by LATTICES:def 5

            .= ((b ` ) + b) by Def7

            .= ((a ` ) + a) by Th4;

            hence thesis;

          end;

          hence IT = (a + (a ` )) by A1, LATTICES:def 17;

        end;

        given a be Element of L such that

         A2: IT = (a + (a ` ));

        

         A3: for b be Element of L holds ((a + (a ` )) + b) = (a + (a ` ))

        proof

          let b be Element of L;

          ((a + (a ` )) + b) = ((b + (b ` )) + b) by Th4

          .= ((b ` ) + (b + b)) by LATTICES:def 5

          .= ((b ` ) + b) by Def7

          .= ((a ` ) + a) by Th4;

          hence thesis;

        end;

        then for b be Element of L holds (b + (a + (a ` ))) = (a + (a ` ));

        hence thesis by A2, A3, LATTICES:def 17;

      end;

    end

    theorem :: ROBBINS1:7

    

     Th7: for L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr holds ex c be Element of L st for a be Element of L holds (c *' a) = c & ((a + (a ` )) ` ) = c

    proof

      let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr;

      set b = the Element of L;

      take c = (((b ` ) + b) ` );

      let a be Element of L;

      

      thus (c *' a) = ((((b ` ) + b) + (a ` )) ` ) by Th3

      .= ((((a ` ) + a) + (a ` )) ` ) by Th4

      .= ((a + ((a ` ) + (a ` ))) ` ) by LATTICES:def 5

      .= ((a + (a ` )) ` ) by Def7

      .= c by Th4;

      thus thesis by Th4;

    end;

    definition

      let L be join-commutative join-associative non empty ComplLLattStr;

      let x,y be Element of L;

      :: original: *'

      redefine

      func x *' y;

      commutativity

      proof

        let a,b be Element of L;

        

        thus (a *' b) = (((a ` ) + (b ` )) ` )

        .= (b *' a);

      end;

    end

    definition

      let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr;

      :: ROBBINS1:def9

      func Bot L -> Element of L means

      : Def9: for a be Element of L holds (it *' a) = it ;

      existence

      proof

        ex c be Element of L st for a be Element of L holds (c *' a) = c & ((a + (a ` )) ` ) = c by Th7;

        hence thesis;

      end;

      uniqueness

      proof

        let c1,c2 be Element of L such that

         A1: for a be Element of L holds (c1 *' a) = c1 and

         A2: for a be Element of L holds (c2 *' a) = c2;

        

        thus c1 = (c2 *' c1) by A1

        .= c2 by A2;

      end;

    end

    theorem :: ROBBINS1:8

    

     Th8: for L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr, a be Element of L holds ( Bot L) = ((a + (a ` )) ` )

    proof

      let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr, a be Element of L;

      for b be Element of L holds (((a + (a ` )) ` ) *' b) = ((a + (a ` )) ` )

      proof

        let b be Element of L;

        (((a + (a ` )) ` ) *' b) = (((((b + (b ` )) ` ) ` ) + (b ` )) ` ) by Th4

        .= (((b + (b ` )) + (b ` )) ` ) by Th3

        .= ((b + ((b ` ) + (b ` ))) ` ) by LATTICES:def 5

        .= ((b + (b ` )) ` ) by Def7

        .= (((a ` ) + a) ` ) by Th4;

        hence thesis;

      end;

      hence thesis by Def9;

    end;

    theorem :: ROBBINS1:9

    

     Th9: for L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr holds (( Top L) ` ) = ( Bot L) & ( Top L) = (( Bot L) ` )

    proof

      let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr;

      set a = the Element of L;

      

      thus (( Top L) ` ) = ((a + (a ` )) ` ) by Def8

      .= ( Bot L) by Th8;

      hence thesis by Th3;

    end;

    theorem :: ROBBINS1:10

    

     Th10: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L st (a ` ) = (b ` ) holds a = b

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L;

      assume

       A1: (a ` ) = (b ` );

      

      thus a = ((a ` ) ` ) by Th3

      .= b by A1, Th3;

    end;

    theorem :: ROBBINS1:11

    

     Th11: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L holds (a + ((b + (b ` )) ` )) = a

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L;

      set O = (b + (b ` ));

      

       A1: ((O ` ) ` ) = O by Th3;

      

       A2: (O ` ) = (((((O ` ) ` ) + ((O ` ) ` )) ` ) + ((((O ` ) ` ) + (O ` )) ` )) by Def6

      .= (((O + O) ` ) + (O ` )) by A1, Th4;

      

       A3: O = ((a ` ) + a) by Th4;

      O = (O + (O ` )) by Th4

      .= ((O + (O ` )) + ((O + O) ` )) by A2, LATTICES:def 5

      .= (O + ((O + O) ` )) by Th4;

      

      then

       A4: (O + O) = ((O + O) + ((O + O) ` )) by LATTICES:def 5

      .= O by Th4;

      

      hence (a + (O ` )) = (((((a ` ) + (a ` )) ` ) + (((a ` ) + a) ` )) + ((((a ` ) + a) ` ) + (((a ` ) + a) ` ))) by A2, A3, Def6

      .= ((((a ` ) + (a ` )) ` ) + ((((a ` ) + a) ` ) + (((a ` ) + a) ` ))) by A2, A4, A3, LATTICES:def 5

      .= a by A2, A4, A3, Def6;

    end;

    theorem :: ROBBINS1:12

    

     Th12: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L holds (a + a) = a

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L;

      

       A1: ((a + a) ` ) = (((((a ` ) ` ) + (a ` )) ` ) + ((a + a) ` )) by Th11

      .= (((((a ` ) ` ) + (a ` )) ` ) + ((((a ` ) ` ) + a) ` )) by Th3

      .= (a ` ) by Def6;

      

      thus (a + a) = (((a + a) ` ) ` ) by Th3

      .= a by A1, Th3;

    end;

    registration

      cluster join-commutative join-associative Huntington -> join-idempotent for non empty ComplLLattStr;

      coherence by Th12;

    end

    theorem :: ROBBINS1:13

    

     Th13: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L holds (a + ( Bot L)) = a

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L;

      a = ((((a ` ) + (a ` )) ` ) + (((a ` ) + a) ` )) by Def6

      .= (((a ` ) ` ) + (((a ` ) + a) ` )) by Def7

      .= (a + (((a ` ) + a) ` )) by Th3;

      hence thesis by Th8;

    end;

    theorem :: ROBBINS1:14

    for L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L holds (a *' ( Top L)) = a

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L;

      (a *' ( Top L)) = (((a ` ) + ( Bot L)) ` ) by Th9

      .= ((a ` ) ` ) by Th13

      .= a by Th3;

      hence thesis;

    end;

    theorem :: ROBBINS1:15

    

     Th15: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L holds (a *' (a ` )) = ( Bot L)

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L;

      

      thus (a *' (a ` )) = (( Top L) ` ) by Def8

      .= ( Bot L) by Th9;

    end;

    theorem :: ROBBINS1:16

    

     Th16: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L holds (a *' (b *' c)) = ((a *' b) *' c)

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L;

      

      thus ((a *' b) *' c) = ((((a ` ) + (b ` )) + (c ` )) ` ) by Th3

      .= (((a ` ) + ((b ` ) + (c ` ))) ` ) by LATTICES:def 5

      .= (a *' (b *' c)) by Th3;

    end;

    theorem :: ROBBINS1:17

    

     Th17: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L holds (a + b) = (((a ` ) *' (b ` )) ` )

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L;

      ((a ` ) *' (b ` )) = ((((a ` ) ` ) + b) ` ) by Th3

      .= ((a + b) ` ) by Th3;

      hence thesis by Th3;

    end;

    theorem :: ROBBINS1:18

    for L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L holds (a *' a) = a

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L;

      

      thus (a *' a) = ((a ` ) ` ) by Def7

      .= a by Th3;

    end;

    theorem :: ROBBINS1:19

    for L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L holds (a + ( Top L)) = ( Top L)

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a be Element of L;

      

      thus (a + ( Top L)) = (a + (a + (a ` ))) by Def8

      .= ((a + a) + (a ` )) by LATTICES:def 5

      .= (a + (a ` )) by Def7

      .= ( Top L) by Def8;

    end;

    theorem :: ROBBINS1:20

    

     Th20: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L holds (a + (a *' b)) = a

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L;

      

      thus (a + (a *' b)) = ((a *' b) + ((a *' b) + (a *' (b ` )))) by Def6

      .= (((a *' b) + (a *' b)) + (a *' (b ` ))) by LATTICES:def 5

      .= ((a *' b) + (a *' (b ` ))) by Def7

      .= a by Def6;

    end;

    theorem :: ROBBINS1:21

    

     Th21: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L holds (a *' (a + b)) = a

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L;

      

      thus (a *' (a + b)) = (((a ` ) + ((((a ` ) *' (b ` )) ` ) ` )) ` ) by Th17

      .= (((a ` ) + ((a ` ) *' (b ` ))) ` ) by Th3

      .= ((a ` ) ` ) by Th20

      .= a by Th3;

    end;

    theorem :: ROBBINS1:22

    

     Th22: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L st ((a ` ) + b) = ( Top L) & ((b ` ) + a) = ( Top L) holds a = b

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L;

      assume

       A1: ((a ` ) + b) = ( Top L) & ((b ` ) + a) = ( Top L);

      

      thus a = ((((a ` ) + (b ` )) ` ) + (((a ` ) + b) ` )) by Def6

      .= b by A1, Def6;

    end;

    theorem :: ROBBINS1:23

    

     Th23: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L st (a + b) = ( Top L) & (a *' b) = ( Bot L) holds (a ` ) = b

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L;

      assume (a + b) = ( Top L);

      then

       A1: (((a ` ) ` ) + b) = ( Top L) by Th3;

      assume

       A2: (a *' b) = ( Bot L);

      ((b ` ) + (a ` )) = ((((a ` ) + (b ` )) ` ) ` ) by Th3

      .= ( Top L) by A2, Th9;

      hence thesis by A1, Th22;

    end;

    theorem :: ROBBINS1:24

    

     Th24: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L holds (((((((((a *' b) *' c) + ((a *' b) *' (c ` ))) + ((a *' (b ` )) *' c)) + ((a *' (b ` )) *' (c ` ))) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` ))) = ( Top L)

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L;

      set A = ((a *' b) *' c), B = ((a *' b) *' (c ` )), C = ((a *' (b ` )) *' c);

      set D = ((a *' (b ` )) *' (c ` )), E = (((a ` ) *' b) *' c), F = (((a ` ) *' b) *' (c ` ));

      set G = (((a ` ) *' (b ` )) *' c), H = (((a ` ) *' (b ` )) *' (c ` ));

      (((((((A + B) + C) + D) + E) + F) + G) + H) = (((((((a *' b) + C) + D) + E) + F) + G) + H) by Def6

      .= ((((((a *' b) + (C + D)) + E) + F) + G) + H) by LATTICES:def 5

      .= ((((((a *' b) + (a *' (b ` ))) + E) + F) + G) + H) by Def6

      .= (((((a *' b) + (a *' (b ` ))) + (E + F)) + G) + H) by LATTICES:def 5

      .= (((((a *' b) + (a *' (b ` ))) + ((a ` ) *' b)) + G) + H) by Def6

      .= ((((a *' b) + (a *' (b ` ))) + ((a ` ) *' b)) + (G + H)) by LATTICES:def 5

      .= ((((a *' b) + (a *' (b ` ))) + ((a ` ) *' b)) + ((a ` ) *' (b ` ))) by Def6

      .= ((a + ((a ` ) *' b)) + ((a ` ) *' (b ` ))) by Def6

      .= (a + (((a ` ) *' b) + ((a ` ) *' (b ` )))) by LATTICES:def 5

      .= (a + (a ` )) by Def6;

      hence thesis by Def8;

    end;

    theorem :: ROBBINS1:25

    

     Th25: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L holds ((a *' c) *' (b *' (c ` ))) = ( Bot L) & (((a *' b) *' c) *' (((a ` ) *' b) *' c)) = ( Bot L) & (((a *' (b ` )) *' c) *' (((a ` ) *' b) *' c)) = ( Bot L) & (((a *' b) *' c) *' (((a ` ) *' (b ` )) *' c)) = ( Bot L) & (((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` ))) = ( Bot L)

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L;

      

       A1: for a,b,c be Element of L holds ((a *' c) *' (b *' (c ` ))) = ( Bot L)

      proof

        let a,b,c be Element of L;

        

        thus ((a *' c) *' (b *' (c ` ))) = (((a *' c) *' (c ` )) *' b) by Th16

        .= ((a *' (c *' (c ` ))) *' b) by Th16

        .= ((a *' ( Bot L)) *' b) by Th15

        .= (( Bot L) *' b) by Def9

        .= ( Bot L) by Def9;

      end;

      hence ((a *' c) *' (b *' (c ` ))) = ( Bot L);

      

      thus (((a *' b) *' c) *' (((a ` ) *' b) *' c)) = ((a *' (b *' c)) *' (((a ` ) *' b) *' c)) by Th16

      .= ((((b *' c) *' a) *' ((a ` ) *' b)) *' c) by Th16

      .= (((((b *' c) *' a) *' (a ` )) *' b) *' c) by Th16

      .= ((((b *' c) *' (a *' (a ` ))) *' b) *' c) by Th16

      .= (((b *' c) *' (a *' (a ` ))) *' (b *' c)) by Th16

      .= (((b *' c) *' ( Bot L)) *' (b *' c)) by Th15

      .= (( Bot L) *' (b *' c)) by Def9

      .= ( Bot L) by Def9;

      

      thus (((a *' (b ` )) *' c) *' (((a ` ) *' b) *' c)) = ((a *' ((b ` ) *' c)) *' (((a ` ) *' b) *' c)) by Th16

      .= ((((b ` ) *' c) *' a) *' ((a ` ) *' (b *' c))) by Th16

      .= (((((b ` ) *' c) *' a) *' (a ` )) *' (b *' c)) by Th16

      .= ((((b ` ) *' c) *' (a *' (a ` ))) *' (b *' c)) by Th16

      .= ((((b ` ) *' c) *' ( Bot L)) *' (b *' c)) by Th15

      .= (( Bot L) *' (b *' c)) by Def9

      .= ( Bot L) by Def9;

      

      thus (((a *' b) *' c) *' (((a ` ) *' (b ` )) *' c)) = ((a *' (b *' c)) *' (((a ` ) *' (b ` )) *' c)) by Th16

      .= ((a *' (b *' c)) *' ((a ` ) *' ((b ` ) *' c))) by Th16

      .= ( Bot L) by A1;

      

      thus (((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` ))) = ((a *' (b *' (c ` ))) *' (((a ` ) *' (b ` )) *' (c ` ))) by Th16

      .= ((a *' (b *' (c ` ))) *' ((a ` ) *' ((b ` ) *' (c ` )))) by Th16

      .= ( Bot L) by A1;

    end;

    theorem :: ROBBINS1:26

    

     Th26: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L holds ((a *' b) + (a *' c)) = ((((a *' b) *' c) + ((a *' b) *' (c ` ))) + ((a *' (b ` )) *' c))

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L;

      set A = ((a *' b) *' c);

      (a *' c) = (((a *' c) *' b) + ((a *' c) *' (b ` ))) by Def6

      .= (A + ((a *' c) *' (b ` ))) by Th16

      .= (A + ((a *' (b ` )) *' c)) by Th16;

      

      hence ((a *' b) + (a *' c)) = ((A + ((a *' b) *' (c ` ))) + (A + ((a *' (b ` )) *' c))) by Def6

      .= ((A + (((a *' b) *' (c ` )) + A)) + ((a *' (b ` )) *' c)) by LATTICES:def 5

      .= (((A + A) + ((a *' b) *' (c ` ))) + ((a *' (b ` )) *' c)) by LATTICES:def 5

      .= ((A + ((a *' b) *' (c ` ))) + ((a *' (b ` )) *' c)) by Def7;

    end;

    theorem :: ROBBINS1:27

    

     Th27: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L holds ((a *' (b + c)) ` ) = ((((((a *' (b ` )) *' (c ` )) + (((a ` ) *' b) *' c)) + (((a ` ) *' b) *' (c ` ))) + (((a ` ) *' (b ` )) *' c)) + (((a ` ) *' (b ` )) *' (c ` )))

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L;

      set D = ((a *' (b ` )) *' (c ` )), E = (((a ` ) *' b) *' c), F = (((a ` ) *' b) *' (c ` ));

      set G = (((a ` ) *' (b ` )) *' c), H = (((a ` ) *' (b ` )) *' (c ` ));

      

       A1: (a ` ) = (((a ` ) *' b) + ((a ` ) *' (b ` ))) by Def6

      .= ((E + F) + ((a ` ) *' (b ` ))) by Def6

      .= ((E + F) + (G + H)) by Def6;

      

       A2: ((b ` ) *' (c ` )) = ((a *' ((b ` ) *' (c ` ))) + ((a ` ) *' ((b ` ) *' (c ` )))) by Th1

      .= (D + ((a ` ) *' ((b ` ) *' (c ` )))) by Th16

      .= (D + H) by Th16;

      ((a *' (b + c)) ` ) = ((a ` ) + ((b + c) ` )) by Th3

      .= ((a ` ) + ((((b ` ) *' (c ` )) ` ) ` )) by Th17

      .= ((a ` ) + ((b ` ) *' (c ` ))) by Th3;

      

      hence ((a *' (b + c)) ` ) = ((((E + F) + (G + H)) + H) + D) by A1, A2, LATTICES:def 5

      .= (((((E + F) + G) + H) + H) + D) by LATTICES:def 5

      .= ((((E + F) + G) + (H + H)) + D) by LATTICES:def 5

      .= ((((E + F) + G) + H) + D) by Def7

      .= (D + ((E + F) + (G + H))) by LATTICES:def 5

      .= ((D + (E + F)) + (G + H)) by LATTICES:def 5

      .= (((D + (E + F)) + G) + H) by LATTICES:def 5

      .= ((((D + E) + F) + G) + H) by LATTICES:def 5;

    end;

    theorem :: ROBBINS1:28

    

     Th28: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L holds (((a *' b) + (a *' c)) + ((a *' (b + c)) ` )) = ( Top L)

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L;

      set A = ((a *' b) *' c), B = ((a *' b) *' (c ` )), C = ((a *' (b ` )) *' c);

      set D = ((a *' (b ` )) *' (c ` )), E = (((a ` ) *' b) *' c), F = (((a ` ) *' b) *' (c ` ));

      set G = (((a ` ) *' (b ` )) *' c), H = (((a ` ) *' (b ` )) *' (c ` ));

      set ABC = ((A + B) + C), GH = (G + H);

      ((a *' (b + c)) ` ) = ((((D + E) + F) + G) + H) & ((a *' b) + (a *' c)) = ABC by Th26, Th27;

      

      then (((a *' b) + (a *' c)) + ((a *' (b + c)) ` )) = (ABC + (((D + E) + F) + GH)) by LATTICES:def 5

      .= (ABC + ((D + E) + (F + GH))) by LATTICES:def 5

      .= ((ABC + (D + E)) + (F + GH)) by LATTICES:def 5

      .= (((ABC + D) + E) + (F + GH)) by LATTICES:def 5

      .= ((ABC + D) + (E + (F + GH))) by LATTICES:def 5

      .= ((ABC + D) + (E + ((F + G) + H))) by LATTICES:def 5

      .= (((ABC + D) + E) + ((F + G) + H)) by LATTICES:def 5

      .= (((ABC + D) + E) + (F + GH)) by LATTICES:def 5

      .= ((((ABC + D) + E) + F) + GH) by LATTICES:def 5

      .= (((((ABC + D) + E) + F) + G) + H) by LATTICES:def 5

      .= ( Top L) by Th24;

      hence thesis;

    end;

    theorem :: ROBBINS1:29

    

     Th29: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L holds (((a *' b) + (a *' c)) *' ((a *' (b + c)) ` )) = ( Bot L)

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L;

      set A = ((a *' b) *' c), B = ((a *' b) *' (c ` )), C = ((a *' (b ` )) *' c);

      set D = ((a *' (b ` )) *' (c ` )), E = (((a ` ) *' b) *' c), F = (((a ` ) *' b) *' (c ` ));

      set G = (((a ` ) *' (b ` )) *' c), H = (((a ` ) *' (b ` )) *' (c ` ));

      set DEFG = (((D + E) + F) + G);

      ((A *' D) + (A *' E)) = (( Bot L) + (A *' E)) by Th25

      .= (( Bot L) + ( Bot L)) by Th25

      .= ( Bot L) by Def7;

      

      then ( Top L) = (( Bot L) + ((A *' (D + E)) ` )) by Th28

      .= ((A *' (D + E)) ` ) by Th13;

      

      then ( Bot L) = (((A *' (D + E)) ` ) ` ) by Th9

      .= (A *' (D + E)) by Th3;

      

      then ((A *' (D + E)) + (A *' F)) = (( Bot L) + ( Bot L)) by Th25

      .= ( Bot L) by Def7;

      

      then ( Top L) = (( Bot L) + ((A *' ((D + E) + F)) ` )) by Th28

      .= ((A *' ((D + E) + F)) ` ) by Th13;

      

      then

       A1: ( Bot L) = (((A *' ((D + E) + F)) ` ) ` ) by Th9

      .= (A *' ((D + E) + F)) by Th3;

      (A *' G) = ( Bot L) by Th25;

      then ((A *' ((D + E) + F)) + (A *' G)) = ( Bot L) by A1, Def7;

      

      then ( Top L) = (( Bot L) + ((A *' DEFG) ` )) by Th28

      .= ((A *' DEFG) ` ) by Th13;

      

      then ( Bot L) = (((A *' DEFG) ` ) ` ) by Th9

      .= (A *' DEFG) by Th3;

      

      then ((A *' DEFG) + (A *' H)) = (( Bot L) + ( Bot L)) by Th25

      .= ( Bot L) by Def7;

      

      then

       A2: ( Top L) = (( Bot L) + ((A *' (DEFG + H)) ` )) by Th28

      .= ((A *' (DEFG + H)) ` ) by Th13;

      ((B *' D) + (B *' E)) = (( Bot L) + (B *' E)) by Th25

      .= (( Bot L) + ( Bot L)) by Th25

      .= ( Bot L) by Def7;

      

      then ( Top L) = (( Bot L) + ((B *' (D + E)) ` )) by Th28

      .= ((B *' (D + E)) ` ) by Th13;

      

      then ( Bot L) = (((B *' (D + E)) ` ) ` ) by Th9

      .= (B *' (D + E)) by Th3;

      

      then ((B *' (D + E)) + (B *' F)) = (( Bot L) + ( Bot L)) by Th25

      .= ( Bot L) by Def7;

      

      then ( Top L) = (( Bot L) + ((B *' ((D + E) + F)) ` )) by Th28

      .= ((B *' ((D + E) + F)) ` ) by Th13;

      

      then ( Bot L) = (((B *' ((D + E) + F)) ` ) ` ) by Th9

      .= (B *' ((D + E) + F)) by Th3;

      

      then ((B *' ((D + E) + F)) + (B *' G)) = (( Bot L) + ( Bot L)) by Th25

      .= ( Bot L) by Def7;

      

      then ( Top L) = (( Bot L) + ((B *' DEFG) ` )) by Th28

      .= ((B *' DEFG) ` ) by Th13;

      

      then

       A3: ( Bot L) = (((B *' DEFG) ` ) ` ) by Th9

      .= (B *' DEFG) by Th3;

      (C *' D) = ( Bot L) by Th25;

      

      then ((C *' D) + (C *' E)) = (( Bot L) + ( Bot L)) by Th25

      .= ( Bot L) by Def7;

      

      then ( Top L) = (( Bot L) + ((C *' (D + E)) ` )) by Th28

      .= ((C *' (D + E)) ` ) by Th13;

      

      then ( Bot L) = (((C *' (D + E)) ` ) ` ) by Th9

      .= (C *' (D + E)) by Th3;

      

      then ((C *' (D + E)) + (C *' F)) = (( Bot L) + ( Bot L)) by Th25

      .= ( Bot L) by Def7;

      

      then ( Top L) = (( Bot L) + ((C *' ((D + E) + F)) ` )) by Th28

      .= ((C *' ((D + E) + F)) ` ) by Th13;

      

      then ( Bot L) = (((C *' ((D + E) + F)) ` ) ` ) by Th9

      .= (C *' ((D + E) + F)) by Th3;

      

      then ((C *' ((D + E) + F)) + (C *' G)) = (( Bot L) + ( Bot L)) by Th25

      .= ( Bot L) by Def7;

      

      then ( Top L) = (( Bot L) + ((C *' DEFG) ` )) by Th28

      .= ((C *' DEFG) ` ) by Th13;

      

      then ( Bot L) = (((C *' DEFG) ` ) ` ) by Th9

      .= (C *' DEFG) by Th3;

      

      then ((C *' DEFG) + (C *' H)) = (( Bot L) + ( Bot L)) by Th25

      .= ( Bot L) by Def7;

      

      then

       A4: ( Top L) = (( Bot L) + ((C *' (DEFG + H)) ` )) by Th28

      .= ((C *' (DEFG + H)) ` ) by Th13;

      (B *' H) = ( Bot L) by Th25;

      then ((B *' DEFG) + (B *' H)) = ( Bot L) by A3, Def7;

      

      then

       A5: ( Top L) = (( Bot L) + ((B *' (DEFG + H)) ` )) by Th28

      .= ((B *' (DEFG + H)) ` ) by Th13;

      

       A6: (B *' (DEFG + H)) = (((B *' (DEFG + H)) ` ) ` ) by Th3

      .= ( Bot L) by A5, Th9;

      (A *' (DEFG + H)) = (((A *' (DEFG + H)) ` ) ` ) by Th3

      .= ( Bot L) by A2, Th9;

      then ((A *' (DEFG + H)) + (B *' (DEFG + H))) = ( Bot L) by A6, Def7;

      

      then ( Top L) = (( Bot L) + (((A + B) *' (DEFG + H)) ` )) by Th28

      .= (((A + B) *' (DEFG + H)) ` ) by Th13;

      

      then

       A7: ( Bot L) = ((((A + B) *' (DEFG + H)) ` ) ` ) by Th9

      .= ((A + B) *' (DEFG + H)) by Th3;

      (C *' (DEFG + H)) = (((C *' (DEFG + H)) ` ) ` ) by Th3

      .= ( Bot L) by A4, Th9;

      then (((A + B) *' (DEFG + H)) + (C *' (DEFG + H))) = ( Bot L) by A7, Def7;

      

      then ( Top L) = (( Bot L) + ((((A + B) + C) *' (DEFG + H)) ` )) by Th28

      .= ((((A + B) + C) *' (DEFG + H)) ` ) by Th13;

      

      then

       A8: ( Bot L) = (((((A + B) + C) *' (DEFG + H)) ` ) ` ) by Th9

      .= (((A + B) + C) *' (DEFG + H)) by Th3;

      ((a *' (b + c)) ` ) = (DEFG + H) by Th27;

      hence thesis by A8, Th26;

    end;

    theorem :: ROBBINS1:30

    

     Th30: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L holds (a *' (b + c)) = ((a *' b) + (a *' c))

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L;

      (((a *' b) + (a *' c)) + ((a *' (b + c)) ` )) = ( Top L) & (((a *' b) + (a *' c)) *' ((a *' (b + c)) ` )) = ( Bot L) by Th28, Th29;

      then (((a *' b) + (a *' c)) ` ) = ((a *' (b + c)) ` ) by Th23;

      hence thesis by Th10;

    end;

    theorem :: ROBBINS1:31

    for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L holds (a + (b *' c)) = ((a + b) *' (a + c))

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b,c be Element of L;

      

      thus (a + (b *' c)) = (((a ` ) *' ((((b ` ) + (c ` )) ` ) ` )) ` ) by Th17

      .= (((a ` ) *' ((b ` ) + (c ` ))) ` ) by Th3

      .= ((((a ` ) *' (b ` )) + ((a ` ) *' (c ` ))) ` ) by Th30

      .= ((((((a ` ) *' (b ` )) ` ) *' (((a ` ) *' (c ` )) ` )) ` ) ` ) by Th17

      .= ((((a ` ) *' (b ` )) ` ) *' (((a ` ) *' (c ` )) ` )) by Th3

      .= ((a + b) *' (((a ` ) *' (c ` )) ` )) by Th17

      .= ((a + b) *' (a + c)) by Th17;

    end;

    begin

    definition

      let L be non empty OrthoLattStr;

      :: ROBBINS1:def10

      attr L is well-complemented means

      : Def10: for a be Element of L holds (a ` ) is_a_complement_of a;

    end

    registration

      cluster TrivOrtLat -> Boolean well-complemented;

      coherence

      proof

        set L = TrivOrtLat ;

        thus L is bounded;

        thus L is complemented

        proof

          let b be Element of L;

          take a = b;

          (a "\/" b) = ( Top L) & (a "/\" b) = ( Bottom L) by STRUCT_0:def 10;

          hence thesis;

        end;

        thus L is distributive by STRUCT_0:def 10;

        let a be Element of L;

        

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

        ((a ` ) "\/" a) = ( Top L) & ((a ` ) "/\" a) = ( Bottom L) by STRUCT_0:def 10;

        hence (a ` ) is_a_complement_of a by A1;

      end;

    end

    definition

      mode preOrthoLattice is Lattice-like non empty OrthoLattStr;

    end

    registration

      cluster strict Boolean well-complemented for preOrthoLattice;

      existence

      proof

        take TrivOrtLat ;

        thus thesis;

      end;

    end

    theorem :: ROBBINS1:32

    

     Th32: for L be distributive well-complemented preOrthoLattice, x be Element of L holds ((x ` ) ` ) = x

    proof

      let L be distributive well-complemented preOrthoLattice;

      let x be Element of L;

      ((x ` ) ` ) is_a_complement_of (x ` ) by Def10;

      then

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

      (x ` ) is_a_complement_of x by Def10;

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

      hence thesis by A1, LATTICES: 12;

    end;

    theorem :: ROBBINS1:33

    

     Th33: for L be bounded distributive well-complemented preOrthoLattice, x,y be Element of L holds (x "/\" y) = (((x ` ) "\/" (y ` )) ` )

    proof

      let L be bounded distributive well-complemented preOrthoLattice;

      let x,y be Element of L;

      

       A1: ((x ` ) "\/" ( Top L)) = ( Top L);

      

       A2: ((y ` ) "\/" ( Top L)) = ( Top L);

      

       A3: (y ` ) is_a_complement_of y by Def10;

      then

       A4: ((y ` ) "\/" y) = ( Top L);

      ((x "/\" y) ` ) is_a_complement_of (x "/\" y) by Def10;

      then

       A5: (((x "/\" y) ` ) "\/" (x "/\" y)) = ( Top L) & (((x "/\" y) ` ) "/\" (x "/\" y)) = ( Bottom L);

      

       A6: (x ` ) is_a_complement_of x by Def10;

      then

       A7: ((x ` ) "\/" x) = ( Top L);

      

       A8: ((y ` ) "/\" y) = ( Bottom L) by A3;

      

       A9: ((x ` ) "/\" x) = ( Bottom L) by A6;

      

       A10: (((x ` ) "\/" (y ` )) "/\" (x "/\" y)) = (((x "/\" y) "/\" (x ` )) "\/" ((x "/\" y) "/\" (y ` ))) by LATTICES:def 11

      .= ((y "/\" (x "/\" (x ` ))) "\/" ((x "/\" y) "/\" (y ` ))) by LATTICES:def 7

      .= ((y "/\" ( Bottom L)) "\/" (x "/\" (y "/\" (y ` )))) by A9, LATTICES:def 7

      .= (( Bottom L) "\/" (x "/\" ( Bottom L))) by A8

      .= (( Bottom L) "\/" ( Bottom L))

      .= ( Bottom L);

      (((x ` ) "\/" (y ` )) "\/" (x "/\" y)) = ((((x ` ) "\/" (y ` )) "\/" x) "/\" (((x ` ) "\/" (y ` )) "\/" y)) by LATTICES: 11

      .= ((((y ` ) "\/" (x ` )) "\/" x) "/\" ( Top L)) by A4, A1, LATTICES:def 5

      .= (( Top L) "/\" ( Top L)) by A7, A2, LATTICES:def 5

      .= ( Top L);

      then ((x "/\" y) ` ) = ((x ` ) "\/" (y ` )) by A10, A5, LATTICES: 12;

      hence thesis by Th32;

    end;

    begin

    definition

      let L be non empty ComplLLattStr;

      :: ROBBINS1:def11

      func CLatt L -> strict OrthoLattStr means

      : Def11: the carrier of it = the carrier of L & the L_join of it = the L_join of L & the Compl of it = the Compl of L & for a,b be Element of L holds (the L_meet of it . (a,b)) = (a *' b);

      existence

      proof

        deffunc F( Element of L, Element of L) = ($1 *' $2);

        consider K be BinOp of the carrier of L such that

         A1: for a,b be Element of L holds (K . (a,b)) = F(a,b) from BINOP_1:sch 4;

        take OrthoLattStr (# the carrier of L, the L_join of L, K, the Compl of L #);

        thus thesis by A1;

      end;

      uniqueness

      proof

        let L1,L2 be strict OrthoLattStr such that

         A2: the carrier of L1 = the carrier of L and

         A3: the L_join of L1 = the L_join of L & the Compl of L1 = the Compl of L and

         A4: for a,b be Element of L holds (the L_meet of L1 . (a,b)) = (a *' b) and

         A5: the carrier of L2 = the carrier of L and

         A6: the L_join of L2 = the L_join of L & the Compl of L2 = the Compl of L and

         A7: for a,b be Element of L holds (the L_meet of L2 . (a,b)) = (a *' b);

        reconsider A = the L_meet of L1, B = the L_meet of L2 as BinOp of the carrier of L by A2, A5;

        now

          let a,b be Element of L;

          

          thus (A . (a,b)) = (a *' b) by A4

          .= (B . (a,b)) by A7;

        end;

        hence thesis by A2, A3, A5, A6, BINOP_1: 2;

      end;

    end

    registration

      let L be non empty ComplLLattStr;

      cluster ( CLatt L) -> non empty;

      coherence

      proof

        the carrier of ( CLatt L) = the carrier of L by Def11;

        hence thesis;

      end;

    end

    registration

      let L be join-commutative non empty ComplLLattStr;

      cluster ( CLatt L) -> join-commutative;

      coherence

      proof

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

        the carrier of L = the carrier of ( CLatt L) & the L_join of L = the L_join of ( CLatt L) by Def11;

        hence thesis by BINOP_1:def 2;

      end;

    end

    registration

      let L be join-associative non empty ComplLLattStr;

      cluster ( CLatt L) -> join-associative;

      coherence

      proof

        set K = the L_join of L, M = the L_join of ( CLatt L);

        let a,b,c be Element of ( CLatt L);

        the carrier of L = the carrier of ( CLatt L) & K = M by Def11;

        hence thesis by BINOP_1:def 3;

      end;

    end

    registration

      let L be join-commutative join-associative non empty ComplLLattStr;

      cluster ( CLatt L) -> meet-commutative;

      coherence

      proof

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

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

        

        thus (a "/\" b) = (b9 *' a9) by Def11

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

      end;

    end

    theorem :: ROBBINS1:34

    for L be non empty ComplLLattStr, a,b be Element of L, a9,b9 be Element of ( CLatt L) st a = a9 & b = b9 holds (a *' b) = (a9 "/\" b9) & (a + b) = (a9 "\/" b9) & (a ` ) = (a9 ` ) by Def11;

    registration

      let L be join-commutative join-associative Huntington non empty ComplLLattStr;

      cluster ( CLatt L) -> meet-associative join-absorbing meet-absorbing;

      coherence

      proof

        hereby

          let a,b,c be Element of ( CLatt L);

          reconsider a9 = a, b9 = b, c9 = c as Element of L by Def11;

          

           A1: (b9 *' c9) = (b "/\" c) by Def11;

          (a9 *' b9) = (a "/\" b) by Def11;

          

          hence ((a "/\" b) "/\" c) = ((a9 *' b9) *' c9) by Def11

          .= (a9 *' (b9 *' c9)) by Th16

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

        end;

        hereby

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

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

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

          

          hence (a "/\" (a "\/" b)) = (a9 *' (a9 + b9)) by Def11

          .= a by Th21;

        end;

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

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

        (a9 *' b9) = (a "/\" b) by Def11;

        

        hence ((a "/\" b) "\/" b) = ((a9 *' b9) + b9) by Def11

        .= b by Th20;

      end;

    end

    registration

      let L be Huntington non empty ComplLLattStr;

      cluster ( CLatt L) -> Huntington;

      coherence

      proof

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

        reconsider x9 = x, y9 = y as Element of L by Def11;

        

         A1: (x ` ) = (x9 ` ) by Def11;

        (y ` ) = (y9 ` ) by Def11;

        then ((x ` ) + (y ` )) = ((x9 ` ) + (y9 ` )) by A1, Def11;

        then

         A2: (((x ` ) + (y ` )) ` ) = (((x9 ` ) + (y9 ` )) ` ) by Def11;

        ((x ` ) + y) = ((x9 ` ) + y9) by A1, Def11;

        then (((x ` ) + y) ` ) = (((x9 ` ) + y9) ` ) by Def11;

        

        hence ((((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` )) = ((((x9 ` ) + (y9 ` )) ` ) + (((x9 ` ) + y9) ` )) by A2, Def11

        .= x by Def6;

      end;

    end

    registration

      let L be join-commutative join-associative Huntington non empty ComplLLattStr;

      cluster ( CLatt L) -> lower-bounded;

      coherence

      proof

        thus ( CLatt L) is lower-bounded

        proof

          set c9 = ( Bot L);

          reconsider c = c9 as Element of ( CLatt L) by Def11;

          take c;

          let a be Element of ( CLatt L);

          reconsider a9 = a as Element of L by Def11;

          

          thus (c "/\" a) = (c9 *' a9) by Def11

          .= c by Def9;

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

        end;

      end;

    end

    theorem :: ROBBINS1:35

    

     Th35: for L be join-commutative join-associative Huntington non empty ComplLLattStr holds ( Bot L) = ( Bottom ( CLatt L))

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr;

      reconsider C = ( Bot L) as Element of ( CLatt L) by Def11;

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

      proof

        let a be Element of ( CLatt L);

        reconsider a9 = a as Element of L by Def11;

        

        thus (C "/\" a) = (( Bot L) *' a9) by Def11

        .= C by Def9;

        hence thesis;

      end;

      hence thesis by LATTICES:def 16;

    end;

    registration

      let L be join-commutative join-associative Huntington non empty ComplLLattStr;

      cluster ( CLatt L) -> complemented distributive bounded;

      coherence

      proof

        thus ( CLatt L) is complemented

        proof

          let b be Element of ( CLatt L);

          take a = (b ` );

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

          thus (a + b) = ( Top ( CLatt L)) by Def8;

          thus (b + a) = ( Top ( CLatt L)) by Def8;

          

           A1: (a9 ` ) = (a ` ) by Def11

          .= b9 by Th3;

          

          thus (a "/\" b) = (a9 *' b9) by Def11

          .= ( Bot L) by A1, Th8

          .= ( Bottom ( CLatt L)) by Th35;

          hence (b "/\" a) = ( Bottom ( CLatt L));

        end;

        hereby

          let a,b,c be Element of ( CLatt L);

          reconsider a9 = a, b9 = b, c9 = c as Element of L by Def11;

          

           A2: (a "/\" b) = (a9 *' b9) & (a "/\" c) = (a9 *' c9) by Def11;

          (b9 + c9) = (b "\/" c) by Def11;

          

          hence (a "/\" (b "\/" c)) = (a9 *' (b9 + c9)) by Def11

          .= ((a9 *' b9) + (a9 *' c9)) by Th30

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

        end;

        thus ( CLatt L) is lower-bounded;

        thus thesis;

      end;

    end

    begin

    notation

      let G be non empty ComplLLattStr, x be Element of G;

      synonym - x for x ` ;

    end

    definition

      let G be join-commutative non empty ComplLLattStr;

      :: original: Huntington

      redefine

      :: ROBBINS1:def12

      attr G is Huntington means for x,y be Element of G holds (( - (( - x) + ( - y))) + ( - (x + ( - y)))) = y;

      compatibility

      proof

        thus G is Huntington implies for x,y be Element of G holds (( - (( - x) + ( - y))) + ( - (x + ( - y)))) = y;

        assume

         A1: for x,y be Element of G holds (( - (( - x) + ( - y))) + ( - (x + ( - y)))) = y;

        let x,y be Element of G;

        ((((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` )) = x by A1;

        hence thesis;

      end;

    end

    definition

      let G be non empty ComplLLattStr;

      :: ROBBINS1:def13

      attr G is with_idempotent_element means ex x be Element of G st (x + x) = x;

      correctness ;

    end

    reserve G for Robbins join-associative join-commutative non empty ComplLLattStr;

    reserve x,y,z,u,v for Element of G;

    definition

      let G be non empty ComplLLattStr, x,y be Element of G;

      :: ROBBINS1:def14

      func \delta (x,y) -> Element of G equals ( - (( - x) + y));

      coherence ;

    end

    definition

      let G be non empty ComplLLattStr, x,y be Element of G;

      :: ROBBINS1:def15

      func Expand (x,y) -> Element of G equals ( \delta ((x + y),( \delta (x,y))));

      coherence ;

    end

    definition

      let G be non empty ComplLLattStr, x be Element of G;

      :: ROBBINS1:def16

      func x _0 -> Element of G equals ( - (( - x) + x));

      coherence ;

      :: ROBBINS1:def17

      func Double x -> Element of G equals (x + x);

      coherence ;

    end

    definition

      let G be non empty ComplLLattStr, x be Element of G;

      :: ROBBINS1:def18

      func x _1 -> Element of G equals ((x _0 ) + x);

      coherence ;

      :: ROBBINS1:def19

      func x _2 -> Element of G equals ((x _0 ) + ( Double x));

      coherence ;

      :: ROBBINS1:def20

      func x _3 -> Element of G equals ((x _0 ) + (( Double x) + x));

      coherence ;

      :: ROBBINS1:def21

      func x _4 -> Element of G equals ((x _0 ) + (( Double x) + ( Double x)));

      coherence ;

    end

    theorem :: ROBBINS1:36

    

     Th36: ( \delta ((x + y),( \delta (x,y)))) = y

    proof

      

      thus ( \delta ((x + y),( \delta (x,y)))) = ( - (( - (x + y)) + ( - (( - x) + y))))

      .= y by Def5;

    end;

    theorem :: ROBBINS1:37

    ( Expand (x,y)) = y by Th36;

    theorem :: ROBBINS1:38

    ( \delta ((( - x) + y),z)) = ( - (( \delta (x,y)) + z));

    theorem :: ROBBINS1:39

    ( \delta (x,x)) = (x _0 );

    theorem :: ROBBINS1:40

    

     Th40: ( \delta (( Double x),(x _0 ))) = x

    proof

      

      thus ( \delta (( Double x),(x _0 ))) = ( Expand (x,x))

      .= x by Th36;

    end;

    theorem :: ROBBINS1:41

    

     Th41: ( \delta ((x _2 ),x)) = (x _0 )

    proof

      

      thus ( \delta ((x _2 ),x)) = ( \delta ((( Double x) + (x _0 )),( \delta (( Double x),(x _0 ))))) by Th40

      .= (x _0 ) by Th36;

    end;

    theorem :: ROBBINS1:42

    

     Th42: ((x _4 ) + (x _0 )) = ((x _3 ) + (x _1 ))

    proof

      

      thus ((x _4 ) + (x _0 )) = ((((x _0 ) + ( Double x)) + ( Double x)) + (x _0 )) by LATTICES:def 5

      .= (((((x _0 ) + ( Double x)) + x) + x) + (x _0 )) by LATTICES:def 5

      .= (((x _3 ) + x) + (x _0 )) by LATTICES:def 5

      .= ((x _3 ) + (x _1 )) by LATTICES:def 5;

    end;

    theorem :: ROBBINS1:43

    

     Th43: ((x _3 ) + (x _0 )) = ((x _2 ) + (x _1 ))

    proof

      

      thus ((x _3 ) + (x _0 )) = ((((x _0 ) + ( Double x)) + x) + (x _0 )) by LATTICES:def 5

      .= ((x _2 ) + (x _1 )) by LATTICES:def 5;

    end;

    theorem :: ROBBINS1:44

    

     Th44: ((x _3 ) + x) = (x _4 )

    proof

      

      thus ((x _3 ) + x) = ((x _0 ) + ((( Double x) + x) + x)) by LATTICES:def 5

      .= (x _4 ) by LATTICES:def 5;

    end;

    theorem :: ROBBINS1:45

    

     Th45: ( \delta ((x _3 ),(x _0 ))) = x

    proof

      

      thus x = ( Expand ((x _2 ),x)) by Th36

      .= ( \delta ((x + (x _2 )),(x _0 ))) by Th41

      .= ( \delta ((x _3 ),(x _0 ))) by LATTICES:def 5;

    end;

    theorem :: ROBBINS1:46

    ( - x) = ( - y) implies ( \delta (x,z)) = ( \delta (y,z));

    theorem :: ROBBINS1:47

    

     Th47: ( \delta (x,( - y))) = ( \delta (y,( - x)))

    proof

      

      thus ( \delta (x,( - y))) = ( - (( - x) + ( - y)))

      .= ( \delta (y,( - x)));

    end;

    theorem :: ROBBINS1:48

    

     Th48: ( \delta ((x _3 ),x)) = (x _0 )

    proof

      set alpha = ((( - (x _3 )) + (x _1 )) + ( - ( Double x)));

      x = ( Expand ((( - (x _3 )) + (x _0 )),x)) by Th36

      .= ( \delta ((( - (x _3 )) + (x _1 )),( - (( \delta ((x _3 ),(x _0 ))) + x)))) by LATTICES:def 5

      .= ( \delta ((( - (x _3 )) + (x _1 )),( - ( Double x)))) by Th45;

      then

       A1: ( - ( Double x)) = ( \delta (((( - (x _3 )) + (x _1 )) + ( - ( Double x))),x)) by Th36;

      

       A2: x = ( \delta (( Double x),(x _0 ))) by Th40

      .= ( \delta ((( - alpha) + x),(x _0 ))) by A1;

      ( - (x _3 )) = ( Expand (((x _1 ) + ( - ( Double x))),( - (x _3 )))) by Th36

      .= ( \delta (((( - (x _3 )) + (x _1 )) + ( - ( Double x))),( \delta (((x _1 ) + ( - ( Double x))),( - (x _3 )))))) by LATTICES:def 5

      .= ( \delta (alpha,( \delta (((x _0 ) + (x + ( Double x))),( \delta (( Double x),(x _1 ))))))) by Th47

      .= ( \delta (alpha,( \delta ((( Double x) + (x _1 )),( \delta (( Double x),(x _1 ))))))) by LATTICES:def 5

      .= ( - (( - alpha) + (x _1 ))) by Th36;

      

      hence ( \delta ((x _3 ),x)) = ( \delta ((( - alpha) + ((x _0 ) + x)),x))

      .= ( Expand ((( - alpha) + x),(x _0 ))) by A2, LATTICES:def 5

      .= (x _0 ) by Th36;

    end;

    theorem :: ROBBINS1:49

    

     Th49: ( \delta (((x _1 ) + (x _3 )),x)) = (x _0 )

    proof

      (x _0 ) = ( Expand ((x _4 ),(x _0 ))) by Th36

      .= ( \delta (((x _4 ) + (x _0 )),( \delta ((x _4 ),( \delta ((x _3 ),x)))))) by Th48

      .= ( \delta (((x _3 ) + (x _1 )),( \delta ((x _4 ),( \delta ((x _3 ),x)))))) by Th42

      .= ( \delta (((x _3 ) + (x _1 )),( Expand ((x _3 ),x)))) by Th44

      .= ( \delta (((x _3 ) + (x _1 )),x)) by Th36;

      hence thesis;

    end;

    theorem :: ROBBINS1:50

    

     Th50: ( \delta (((x _1 ) + (x _2 )),x)) = (x _0 )

    proof

      

      thus (x _0 ) = ( Expand ((x _3 ),(x _0 ))) by Th36

      .= ( \delta (((x _1 ) + (x _2 )),( \delta ((x _3 ),(x _0 ))))) by Th43

      .= ( \delta (((x _1 ) + (x _2 )),x)) by Th45;

    end;

    theorem :: ROBBINS1:51

    

     Th51: ( \delta (((x _1 ) + (x _3 )),(x _0 ))) = x

    proof

      

      thus x = ( Expand (((x _1 ) + (x _2 )),x)) by Th36

      .= ( \delta (((x _1 ) + ((x _2 ) + x)),( \delta (((x _1 ) + (x _2 )),x)))) by LATTICES:def 5

      .= ( \delta (((x _1 ) + (x _3 )),( \delta (((x _1 ) + (x _2 )),x)))) by LATTICES:def 5

      .= ( \delta (((x _1 ) + (x _3 )),(x _0 ))) by Th50;

    end;

    definition

      let G, x;

      :: ROBBINS1:def22

      func \beta x -> Element of G equals ((( - ((x _1 ) + (x _3 ))) + x) + ( - (x _3 )));

      coherence ;

    end

    theorem :: ROBBINS1:52

    

     Th52: ( \delta (( \beta x),x)) = ( - (x _3 ))

    proof

      

      thus ( - (x _3 )) = ( \delta (( \beta x),( \delta ((( - ((x _1 ) + (x _3 ))) + x),( - (x _3 )))))) by Th36

      .= ( \delta (( \beta x),( \delta ((x _3 ),( \delta (((x _1 ) + (x _3 )),x)))))) by Th47

      .= ( \delta (( \beta x),( \delta ((x _3 ),(x _0 ))))) by Th49

      .= ( \delta (( \beta x),x)) by Th45;

    end;

    theorem :: ROBBINS1:53

    

     Th53: ( \delta (( \beta x),x)) = ( - ((x _1 ) + (x _3 )))

    proof

      

      thus ( - ((x _1 ) + (x _3 ))) = ( \delta ((( - ((x _1 ) + (x _3 ))) + (x + ( - (x _3 )))),( \delta ((x + ( - (x _3 ))),( - ((x _1 ) + (x _3 ))))))) by Th36

      .= ( \delta (( \beta x),( \delta ((x + ( - (x _3 ))),( - ((x _1 ) + (x _3 ))))))) by LATTICES:def 5

      .= ( \delta (( \beta x),( \delta (((x _1 ) + (x _3 )),( \delta ((x _3 ),x)))))) by Th47

      .= ( \delta (( \beta x),( \delta (((x _1 ) + (x _3 )),(x _0 ))))) by Th48

      .= ( \delta (( \beta x),x)) by Th51;

    end;

    theorem :: ROBBINS1:54

    ex y, z st ( - (y + z)) = ( - z)

    proof

      set x = the Element of G;

      take y = (x _1 ), z = (x _3 );

      ( - (y + z)) = ( \delta (( \beta x),x)) by Th53

      .= ( - z) by Th52;

      hence thesis;

    end;

    begin

    theorem :: ROBBINS1:55

    (for z holds ( - ( - z)) = z) implies G is Huntington

    proof

      assume

       A1: for z holds ( - ( - z)) = z;

      let x, y;

      

       A2: ( - ( - (( - (( - x) + ( - y))) + ( - (x + ( - y)))))) = ( - ( - y)) by Def5;

      (( - (( - x) + ( - y))) + ( - (x + ( - y)))) = ( - ( - (( - (( - x) + ( - y))) + ( - (x + ( - y)))))) by A1

      .= y by A1, A2;

      hence thesis;

    end;

    theorem :: ROBBINS1:56

    

     Th56: G is with_idempotent_element implies G is Huntington

    proof

      assume G is with_idempotent_element;

      then

      consider C be Element of G such that

       A1: (C + C) = C;

       A2:

      now

        let x;

        

        thus (C + x) = ( - (( - (( - C) + (C + x))) + ( - (C + (C + x))))) by Def5

        .= ( - (( - ((( - C) + C) + x)) + ( - (C + (C + x))))) by LATTICES:def 5

        .= ( - (( - ((C + ( - C)) + x)) + ( - (C + x)))) by A1, LATTICES:def 5;

      end;

      assume G is non Huntington;

      then

      consider B,A be Element of G such that

       A3: (( - (( - B) + ( - A))) + ( - (B + ( - A)))) <> A;

      set D = ((C + ( - C)) + ( - C));

      

       A4: C = ( - (( - C) + ( - (C + ( - C))))) by A1, Def5;

      then

       A5: ( - (C + ( - ((C + ( - C)) + ( - C))))) = ( - C) by Def5;

      

      then ( - (( - C) + ( - ((C + ( - C)) + ( - C))))) = ( - (( - (( - ((C + ( - C)) + ( - C))) + C)) + ( - ((C + C) + (( - C) + ( - C)))))) by A1, LATTICES:def 5

      .= ( - (( - (( - ((C + ( - C)) + ( - C))) + C)) + ( - (C + (C + (( - C) + ( - C))))))) by LATTICES:def 5

      .= ( - (( - (( - D) + C)) + ( - (D + C)))) by LATTICES:def 5

      .= C by Def5;

      then

       A6: ( - (C + ( - C))) = ( - ((C + ( - C)) + ( - C))) by A5, Def5;

      C = ( - (( - (C + C)) + ( - ((( - C) + ( - (C + ( - C)))) + C)))) by A4, Def5

      .= ( - (( - C) + ( - ((C + ( - C)) + ( - (C + ( - C))))))) by A1, LATTICES:def 5;

      then

       A7: C = (C + ( - (C + ( - C)))) by A2, A5, A6;

       A8:

      now

        let x;

        

        thus x = ( - (( - ((C + ( - (C + ( - C)))) + x)) + ( - ((( - C) + ( - (C + ( - C)))) + x)))) by A4, A7, Def5

        .= ( - (( - (C + (( - (C + ( - C))) + x))) + ( - ((( - C) + ( - (C + ( - C)))) + x)))) by LATTICES:def 5

        .= ( - (( - (C + (( - (C + ( - C))) + x))) + ( - (( - C) + (( - (C + ( - C))) + x))))) by LATTICES:def 5

        .= (( - (C + ( - C))) + x) by Def5;

      end;

       A9:

      now

        let x;

        

        thus ( - (C + ( - C))) = ( - (( - (( - x) + ( - (C + ( - C))))) + ( - (x + ( - (C + ( - C))))))) by Def5

        .= ( - (( - ( - x)) + ( - (x + ( - (C + ( - C))))))) by A8

        .= ( - (( - ( - x)) + ( - x))) by A8;

      end;

       A10:

      now

        let x;

        

        thus ( - ( - x)) = ( - (( - (( - x) + ( - ( - x)))) + ( - (x + ( - ( - x)))))) by Def5

        .= ( - (( - (C + ( - C))) + ( - (x + ( - ( - x)))))) by A9

        .= ( - ( - (x + ( - ( - x))))) by A8;

      end;

       A11:

      now

        let x;

        

        thus ( - x) = ( - (( - (( - ( - ( - x))) + ( - x))) + ( - (( - ( - x)) + ( - x))))) by Def5

        .= ( - (( - (( - ( - ( - x))) + ( - x))) + ( - (C + ( - C))))) by A9

        .= ( - ( - (( - ( - ( - x))) + ( - x)))) by A8

        .= ( - ( - ( - x))) by A10;

      end;

       A12:

      now

        let x, y;

        

        thus y = ( - (( - (( - x) + y)) + ( - (x + y)))) by Def5

        .= ( - ( - ( - (( - (( - x) + y)) + ( - (x + y)))))) by A11

        .= ( - ( - y)) by Def5;

      end;

      now

        let x, y;

        

        thus (( - (( - x) + y)) + ( - (x + y))) = ( - ( - (( - (( - x) + y)) + ( - (x + y))))) by A12

        .= ( - y) by Def5;

      end;

      

      then (( - (( - B) + ( - A))) + ( - (B + ( - A)))) = ( - ( - A))

      .= A by A12;

      hence thesis by A3;

    end;

    registration

      cluster TrivComplLat -> with_idempotent_element;

      coherence

      proof

        set x = the Element of TrivComplLat ;

        take x;

        thus x = (x + x) by STRUCT_0:def 10;

      end;

    end

    registration

      cluster with_idempotent_element -> Huntington for Robbins join-associative join-commutative non empty ComplLLattStr;

      coherence by Th56;

    end

    theorem :: ROBBINS1:57

    

     Th57: (ex c,d be Element of G st (c + d) = c) implies G is Huntington

    proof

       A1:

      now

        let x, y, z;

        set k = ( - (( - x) + y));

        

        thus ( - (( - ((( - (( - x) + y)) + x) + y)) + y)) = ( - (( - ((k + x) + y)) + ( - (k + ( - (x + y)))))) by Def5

        .= ( - (( - (k + (x + y))) + ( - (k + ( - (x + y)))))) by LATTICES:def 5

        .= ( - (( - x) + y)) by Def5;

      end;

       A2:

      now

        let x, y, z;

        set k = ( - (( - x) + y));

        ( - (( - ((k + x) + y)) + y)) = k by A1;

        hence z = ( - (( - ((( - ((( - (( - x) + y)) + x) + y)) + y) + z)) + ( - (( - (( - x) + y)) + z)))) by Def5;

      end;

      given C,D be Element of G such that

       A3: (C + D) = C;

       A4:

      now

        let x, y, z;

        set k = (( - (( - x) + y)) + ( - (x + y)));

        

        thus ( - (( - ((( - (( - x) + y)) + ( - (x + y))) + z)) + ( - (y + z)))) = ( - (( - (k + z)) + ( - (( - k) + z)))) by Def5

        .= z by Def5;

      end;

       A5:

      now

        let x;

        

        thus D = ( - (( - ((( - (( - x) + C)) + ( - (x + C))) + D)) + ( - (C + D)))) by A4

        .= ( - (( - C) + ( - ((D + ( - (C + ( - x)))) + ( - (C + x)))))) by A3, LATTICES:def 5;

      end;

      set e = ( - (C + ( - C)));

      set K = ( - ((C + C) + ( - (C + ( - C)))));

      

       A6: K = ( - ((C + ( - (C + ( - C)))) + C)) by LATTICES:def 5;

       A7:

      now

        let x, y;

        

        thus ( - (( - ((D + ( - (C + x))) + y)) + ( - ((C + x) + y)))) = ( - (( - (( - (C + x)) + (D + y))) + ( - (((C + D) + x) + y)))) by A3, LATTICES:def 5

        .= ( - (( - (( - (C + x)) + (D + y))) + ( - (((C + x) + D) + y)))) by LATTICES:def 5

        .= ( - (( - (( - (C + x)) + (D + y))) + ( - ((C + x) + (D + y))))) by LATTICES:def 5

        .= (D + y) by Def5;

      end;

      set L = ( - (D + ( - C)));

      set E = (D + ( - C));

      

       A8: ( - (( - C) + ( - (D + ( - C))))) = D by A3, Def5;

      then

       A9: ( - (D + ( - (C + ( - E))))) = ( - E) by Def5;

      ( - (L + ( - (C + L)))) = ( - (( - (D + ( - (C + L)))) + ( - ((D + C) + L)))) by A3, A8, Def5

      .= ( - (( - (D + ( - (C + L)))) + ( - (D + (C + L))))) by LATTICES:def 5

      .= D by Def5;

      then ( - (D + ( - ((D + ( - C)) + ( - (C + ( - (D + ( - C))))))))) = ( - (C + ( - (D + ( - C))))) by Def5;

      

      then

       A10: ( - (C + ( - (D + ( - C))))) = ( - (D + ( - ((D + ( - (C + ( - (D + ( - C)))))) + ( - C))))) by LATTICES:def 5

      .= ( - C) by A8, A9, Def5;

      set L = (C + ( - (D + ( - C))));

      

       A11: C = ( - (( - ((D + ( - L)) + C)) + ( - (( - (D + ( - C))) + C)))) by A9, Def5

      .= ( - (( - L) + ( - (C + ( - L))))) by A3, LATTICES:def 5;

      then ( - (C + ( - (C + ( - (C + ( - C))))))) = ( - (C + ( - C))) by A10, Def5;

      then C = ( - (( - (C + ( - C))) + K)) by A6, Def5;

      then ( - (C + ( - ((C + ( - C)) + K)))) = K by Def5;

      

      then K = ( - (( - ((K + C) + ( - C))) + C)) by LATTICES:def 5

      .= ( - (( - ((( - ((( - (C + ( - C))) + C) + C)) + C) + ( - C))) + C)) by LATTICES:def 5

      .= ( - C) by A11, A2, A10;

      

      then (D + ( - (C + ( - C)))) = ( - (( - ((D + ( - (C + C))) + ( - (C + ( - C))))) + ( - C))) by A7

      .= ( - (( - C) + ( - ((D + ( - (C + ( - C)))) + ( - (C + C)))))) by LATTICES:def 5

      .= D by A5;

      then

       A12: (C + ( - (C + ( - C)))) = C by A3, LATTICES:def 5;

      now

        let x;

        

        thus x = ( - (( - ((C + ( - (C + ( - C)))) + x)) + ( - ((( - C) + ( - (C + ( - C)))) + x)))) by A11, A10, A12, Def5

        .= ( - (( - (C + (( - (C + ( - C))) + x))) + ( - ((( - C) + ( - (C + ( - C)))) + x)))) by LATTICES:def 5

        .= ( - (( - (C + (( - (C + ( - C))) + x))) + ( - (( - C) + (( - (C + ( - C))) + x))))) by LATTICES:def 5

        .= (( - (C + ( - C))) + x) by Def5;

      end;

      then e = (e + e);

      then G is with_idempotent_element;

      hence thesis;

    end;

    theorem :: ROBBINS1:58

    

     Th58: ex y, z st (y + z) = z

    proof

       A1:

      now

        let x, y;

        

        thus ( - (x + y)) = ( - (( - (( - (( - x) + y)) + ( - (x + y)))) + ( - ((( - x) + y) + ( - (x + y)))))) by Def5

        .= ( - (y + ( - ((( - x) + y) + ( - (x + y)))))) by Def5

        .= ( - (( - ((( - (x + y)) + ( - x)) + y)) + y)) by LATTICES:def 5;

      end;

       A2:

      now

        let x, y;

        

        thus ( - (( - x) + y)) = ( - (( - (( - (x + y)) + ( - (( - x) + y)))) + ( - ((x + y) + ( - (( - x) + y)))))) by Def5

        .= ( - (y + ( - ((x + y) + ( - (( - x) + y)))))) by Def5

        .= ( - (( - ((( - (( - x) + y)) + x) + y)) + y)) by LATTICES:def 5;

      end;

       A3:

      now

        let x, y;

        

        thus y = ( - (( - (( - ((( - (( - x) + y)) + x) + y)) + y)) + ( - (((( - (( - x) + y)) + x) + y) + y)))) by Def5

        .= ( - (( - (( - x) + y)) + ( - (((( - (( - x) + y)) + x) + y) + y)))) by A2

        .= ( - (( - ((( - (( - x) + y)) + x) + ( Double y))) + ( - (( - x) + y)))) by LATTICES:def 5;

      end;

       A4:

      now

        let x, y, z;

        

        thus z = ( - (( - (( - (( - ((( - (( - x) + y)) + x) + ( Double y))) + ( - (( - x) + y)))) + z)) + ( - ((( - ((( - (( - x) + y)) + x) + ( Double y))) + ( - (( - x) + y))) + z)))) by Def5

        .= ( - (( - ((( - ((( - (( - x) + y)) + x) + ( Double y))) + ( - (( - x) + y))) + z)) + ( - (y + z)))) by A3;

      end;

       A5:

      now

        let x, y, z;

        set k = ((( - ((( - (( - x) + y)) + x) + ( Double y))) + ( - (( - x) + y))) + z);

        

        thus ( - (y + z)) = ( - (( - (( - k) + ( - (y + z)))) + ( - (k + ( - (y + z)))))) by Def5

        .= ( - (z + ( - (k + ( - (y + z)))))) by A4

        .= ( - (( - (((( - ((( - (( - x) + y)) + x) + ( Double y))) + ( - (( - x) + y))) + ( - (y + z))) + z)) + z)) by LATTICES:def 5;

      end;

       A6:

      now

        let x, y, z, u;

        set k = (( - (((( - ((( - (( - x) + y)) + x) + ( Double y))) + ( - (( - x) + y))) + ( - (y + z))) + z)) + z);

        

        thus u = ( - (( - (( - k) + u)) + ( - (k + u)))) by Def5

        .= ( - (( - (( - (y + z)) + u)) + ( - (k + u)))) by A5;

      end;

       A7:

      now

        let x, y, z, v;

        set k = ( - (( - (( Double v) + v)) + v));

        set l = (( - (( - (( Double v) + v)) + v)) + ( Double v));

        set v5 = ((( Double v) + ( Double v)) + v);

        

         A8: ( - ((( Double v) + v) + l)) = ( - (( - ((( - ((( Double v) + v) + l)) + ( - (( Double v) + v))) + l)) + l)) by A1

        .= ( - (( - ((( - ((( Double v) + v) + l)) + l) + ( - (( Double v) + v)))) + l)) by LATTICES:def 5;

        

        thus k = ( - (( - (( - (v + ( Double v))) + k)) + ( - ((( - (((( - ((( - (( - (( Double v) + v)) + v)) + (( Double v) + v)) + ( Double v))) + ( - (( - (( Double v) + v)) + v))) + ( - (v + ( Double v)))) + ( Double v))) + ( Double v)) + k)))) by A6

        .= ( - (( - (( - (v + ( Double v))) + k)) + ( - ((( - (((( - (((( Double v) + v) + k) + ( Double v))) + k) + ( Double v)) + ( - (v + ( Double v))))) + ( Double v)) + k)))) by LATTICES:def 5

        .= ( - (( - (( - (v + ( Double v))) + k)) + ( - ((( - ((( - (((( Double v) + v) + k) + ( Double v))) + (k + ( Double v))) + ( - (v + ( Double v))))) + ( Double v)) + k)))) by LATTICES:def 5

        .= ( - (( - (( - (v + ( Double v))) + k)) + ( - ((( - ((( - ((( Double v) + v) + (k + ( Double v)))) + l) + ( - (v + ( Double v))))) + ( Double v)) + k)))) by LATTICES:def 5

        .= ( - (( - (( - (v + ( Double v))) + k)) + ( - (( - ((( - ((( Double v) + v) + l)) + l) + ( - (v + ( Double v))))) + l)))) by LATTICES:def 5

        .= ( - (( - (( - (( Double v) + v)) + k)) + ( - (((( Double v) + v) + ( Double v)) + k)))) by A8, LATTICES:def 5

        .= ( - (( - (( - (( Double v) + v)) + k)) + ( - (v5 + k)))) by LATTICES:def 5;

      end;

       A9:

      now

        let x;

        set k = (( - (( - (( Double x) + x)) + x)) + ( - (( Double x) + x)));

        set l = ( - (( - (( - (( Double x) + x)) + x)) + ((( Double x) + ( Double x)) + x)));

        

         A10: ( - (( Double x) + x)) = ( - (( - ((( - ((( - (( - (( Double x) + x)) + x)) + (( Double x) + x)) + ( Double x))) + ( - (( - (( Double x) + x)) + x))) + ( - (( Double x) + x)))) + ( - (x + ( - (( Double x) + x)))))) by A4

        .= ( - (( - (( - ((( - (( - (( Double x) + x)) + x)) + (( Double x) + x)) + ( Double x))) + k)) + ( - (x + ( - (( Double x) + x)))))) by LATTICES:def 5

        .= ( - (( - (( - (( - (( - (( Double x) + x)) + x)) + ((( Double x) + x) + ( Double x)))) + k)) + ( - (x + ( - (( Double x) + x)))))) by LATTICES:def 5

        .= ( - (( - (l + k)) + ( - (x + ( - (( Double x) + x)))))) by LATTICES:def 5;

        l = ( - (( - (( - k) + l)) + ( - (k + l)))) by Def5

        .= ( - (( - (( - (( Double x) + x)) + x)) + ( - (k + l)))) by A7;

        hence ( - (( - (( - (( Double x) + x)) + x)) + ((( Double x) + ( Double x)) + x))) = ( - (( Double x) + x)) by A10;

      end;

       A11:

      now

        let x;

        

         A12: ( - (( - (( Double x) + x)) + x)) = ( - (( - ((( - (( - (( Double x) + x)) + x)) + (( Double x) + x)) + x)) + x)) by A2

        .= ( - (( - (( - (( - (( Double x) + x)) + x)) + ((( Double x) + x) + x))) + x)) by LATTICES:def 5

        .= ( - (( - (( - (( - (( Double x) + x)) + x)) + (( Double x) + ( Double x)))) + x)) by LATTICES:def 5;

        

        thus x = ( - (( - (( - (( - (( - (( Double x) + x)) + x)) + (( Double x) + ( Double x)))) + x)) + ( - ((( - (( - (( Double x) + x)) + x)) + (( Double x) + ( Double x))) + x)))) by Def5

        .= ( - (( - (( - (( - (( - (( Double x) + x)) + x)) + (( Double x) + ( Double x)))) + x)) + ( - (( - (( - (( Double x) + x)) + x)) + ((( Double x) + ( Double x)) + x))))) by LATTICES:def 5

        .= ( - (( - (( - (( Double x) + x)) + x)) + ( - (( Double x) + x)))) by A9, A12;

      end;

       A13:

      now

        let x, y;

        

        thus y = ( - (( - (( - (( - (( - (( Double x) + x)) + x)) + ( - (( Double x) + x)))) + y)) + ( - ((( - (( - (( Double x) + x)) + x)) + ( - (( Double x) + x))) + y)))) by Def5

        .= ( - (( - ((( - (( - (( Double x) + x)) + x)) + ( - (( Double x) + x))) + y)) + ( - (x + y)))) by A11;

      end;

       A14:

      now

        let x;

        

        thus (( - (( - (( Double x) + x)) + x)) + ( Double x)) = ( - (( - (( - (( Double x) + x)) + (( - (( - (( Double x) + x)) + x)) + ( Double x)))) + ( - ((( Double x) + x) + (( - (( - (( Double x) + x)) + x)) + ( Double x)))))) by Def5

        .= ( - (( - (( - (( Double x) + x)) + (( - (( - (( Double x) + x)) + x)) + ( Double x)))) + ( - (( - (( - (( Double x) + x)) + x)) + ((( Double x) + x) + ( Double x)))))) by LATTICES:def 5

        .= ( - (( - (( - (( Double x) + x)) + (( - (( - (( Double x) + x)) + x)) + ( Double x)))) + ( - (( - (( - (( Double x) + x)) + x)) + ((( Double x) + ( Double x)) + x))))) by LATTICES:def 5

        .= ( - (( - (( - (( Double x) + x)) + (( - (( - (( Double x) + x)) + x)) + ( Double x)))) + ( - (( Double x) + x)))) by A9

        .= ( - (( - ((( - (( - (( Double x) + x)) + x)) + ( - (( Double x) + x))) + ( Double x))) + ( - (( Double x) + x)))) by LATTICES:def 5;

      end;

       A15:

      now

        let x, y;

        

        thus ( Double x) = ( - (( - ((( - (( - (( Double x) + x)) + x)) + ( - (( Double x) + x))) + ( Double x))) + ( - (x + ( Double x))))) by A13

        .= (( - (( - (( Double x) + x)) + x)) + ( Double x)) by A14;

      end;

      set x = the Element of G;

      set c = ( Double x), d = ( - (( - (( Double x) + x)) + x));

      take d, c;

      thus thesis by A15;

    end;

    registration

      cluster Robbins -> Huntington for join-associative join-commutative non empty ComplLLattStr;

      coherence

      proof

        let K be join-associative join-commutative non empty ComplLLattStr;

        assume

         A1: K is Robbins;

        then ex y,z be Element of K st (y + z) = z by Th58;

        hence thesis by A1, Th57;

      end;

    end

    definition

      let L be non empty OrthoLattStr;

      :: ROBBINS1:def23

      attr L is de_Morgan means

      : Def23: for x,y be Element of L holds (x "/\" y) = (((x ` ) "\/" (y ` )) ` );

    end

    registration

      let L be non empty ComplLLattStr;

      cluster ( CLatt L) -> de_Morgan;

      coherence

      proof

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

        reconsider x9 = x, y9 = y as Element of L by Def11;

        (x9 ` ) = (x ` ) & (y9 ` ) = (y ` ) by Def11;

        then ((x9 ` ) "\/" (y9 ` )) = ((x ` ) "\/" (y ` )) by Def11;

        then (((x ` ) "\/" (y ` )) ` ) = (x9 *' y9) by Def11;

        hence thesis by Def11;

      end;

    end

    theorem :: ROBBINS1:59

    

     Th59: for L be well-complemented join-commutative meet-commutative non empty OrthoLattStr, x be Element of L holds (x + (x ` )) = ( Top L) & (x "/\" (x ` )) = ( Bottom L)

    proof

      let L be well-complemented join-commutative meet-commutative non empty OrthoLattStr, x be Element of L;

      

       A1: (x ` ) is_a_complement_of x by Def10;

      hence (x + (x ` )) = ( Top L);

      thus thesis by A1;

    end;

    theorem :: ROBBINS1:60

    

     Th60: for L be bounded distributive well-complemented preOrthoLattice holds (( Top L) ` ) = ( Bottom L)

    proof

      let L be bounded distributive well-complemented preOrthoLattice;

      set x = the Element of L;

      (( Top L) ` ) = ((((x ` ) ` ) + (x ` )) ` ) by Th59

      .= ((x ` ) "/\" x) by Th33

      .= ( Bottom L) by Th59;

      hence thesis;

    end;

    registration

      cluster TrivOrtLat -> de_Morgan;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster strict de_Morgan Boolean Robbins Huntington for preOrthoLattice;

      existence

      proof

        take TrivOrtLat ;

        thus thesis;

      end;

    end

    registration

      cluster join-associative join-commutative de_Morgan -> meet-commutative for non empty OrthoLattStr;

      coherence

      proof

        let L be non empty OrthoLattStr;

        assume L is join-associative join-commutative de_Morgan;

        then

        reconsider L1 = L as join-associative join-commutative de_Morgan non empty OrthoLattStr;

        let a,b be Element of L;

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

        

        thus (a "/\" b) = (a1 *' b1) by Def23

        .= (b1 *' a1)

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

      end;

    end

    theorem :: ROBBINS1:61

    

     Th61: for L be Huntington de_Morgan preOrthoLattice holds ( Bot L) = ( Bottom L)

    proof

      let L be Huntington de_Morgan preOrthoLattice;

      reconsider C = ( Bot L) as Element of L;

      

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

      proof

        let a be Element of L;

        reconsider a9 = a as Element of L;

        

        thus (C "/\" a) = (( Bot L) *' a9) by Def23

        .= C by Def9;

        hence thesis;

      end;

      then L is lower-bounded;

      hence thesis by A1, LATTICES:def 16;

    end;

    registration

      cluster Boolean -> Huntington for well-complemented preOrthoLattice;

      coherence

      proof

        let L be well-complemented preOrthoLattice;

        assume

         A1: L is Boolean;

        then

        reconsider L9 = L as Boolean preOrthoLattice;

        

         A2: for x be Element of L9 holds (( Top L9) "/\" x) = x;

        now

          let x,y be Element of L;

          

          thus ((((x ` ) "\/" (y ` )) ` ) "\/" (((x ` ) "\/" y) ` )) = ((x "/\" y) + (((x ` ) + y) ` )) by A1, Th33

          .= ((x + (((x ` ) + y) ` )) "/\" (y + (((x ` ) + y) ` ))) by A1, LATTICES: 11

          .= ((x + (((x ` ) + ((y ` ) ` )) ` )) "/\" (y + (((x ` ) + y) ` ))) by A1, Th32

          .= ((x + (x "/\" (y ` ))) "/\" (y + (((x ` ) + y) ` ))) by A1, Th33

          .= (x "/\" (y + (((x ` ) + y) ` ))) by LATTICES:def 8

          .= (x "/\" (y + (((x ` ) + ((y ` ) ` )) ` ))) by A1, Th32

          .= (x "/\" (y + (x "/\" (y ` )))) by A1, Th33

          .= (x "/\" ((y + x) "/\" (y + (y ` )))) by A1, LATTICES: 11

          .= ((x "/\" (y + x)) "/\" (y + (y ` ))) by LATTICES:def 7

          .= (x "/\" (y + (y ` ))) by LATTICES:def 9

          .= (x "/\" ( Top L)) by Th59

          .= x by A2;

        end;

        hence thesis;

      end;

    end

    registration

      cluster Huntington -> Boolean for de_Morgan preOrthoLattice;

      coherence

      proof

        let L be de_Morgan preOrthoLattice;

        assume

         A1: L is Huntington;

        then

        reconsider L9 = L as Huntington preOrthoLattice;

        

         A2: L is lower-bounded

        proof

          set c9 = ( Bot L9);

          reconsider c = c9 as Element of L;

          take c;

          let a be Element of L;

          reconsider a9 = a as Element of L9;

          

          thus (c "/\" a) = (c9 *' a9) by Def23

          .= c by Def9;

          

          thus (a "/\" c) = (c9 *' a9) by Def23

          .= c by Def9;

        end;

        L9 is upper-bounded;

        hence L is bounded by A2;

        thus L is complemented

        proof

          let b be Element of L;

          take a = (b ` );

          

           A3: L9 is join-idempotent;

          hence (a + b) = ( Top L) by Def8;

          thus (b + a) = ( Top L) by A3, Def8;

          

          thus (a "/\" b) = (((a ` ) + (b ` )) ` ) by Def23

          .= ( Bot L9) by Th8

          .= ( Bottom L) by Th61;

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

        end;

        thus L is distributive

        proof

          let a,b,c be Element of L;

          

           A4: (a "/\" b) = (a *' b) & (a "/\" c) = (a *' c) by Def23;

          

          thus (a "/\" (b "\/" c)) = (a *' (b + c)) by Def23

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

        end;

      end;

    end

    registration

      cluster Robbins de_Morgan -> Boolean for preOrthoLattice;

      coherence ;

      cluster Boolean -> Robbins for well-complemented preOrthoLattice;

      coherence

      proof

        let L be well-complemented preOrthoLattice;

        assume L is Boolean;

        then

        reconsider L9 = L as Boolean well-complemented preOrthoLattice;

        now

          let x,y be Element of L9;

          

          thus ((((x + y) ` ) + ((x + (y ` )) ` )) ` ) = ((x + y) "/\" (x + (y ` ))) by Th33

          .= (((x + y) "/\" x) + ((x + y) "/\" (y ` ))) by LATTICES:def 11

          .= (((x + y) "/\" x) + ((x "/\" (y ` )) + (y "/\" (y ` )))) by LATTICES:def 11

          .= (((x + y) "/\" x) + ((x "/\" (y ` )) + (((y ` ) + ((y ` ) ` )) ` ))) by Th33

          .= (x + ((x "/\" (y ` )) + (((y ` ) + ((y ` ) ` )) ` ))) by LATTICES:def 9

          .= ((x + (x "/\" (y ` ))) + (((y ` ) + ((y ` ) ` )) ` )) by LATTICES:def 5

          .= (x + (((y ` ) + ((y ` ) ` )) ` )) by LATTICES:def 8

          .= (x + (( Top L9) ` )) by Th59

          .= (x + ( Bottom L9)) by Th60

          .= x;

        end;

        hence thesis;

      end;

    end