The Mizar article:

Robbins Algebras vs. Boolean Algebras

by
Adam Grabowski

Received June 12, 2001

Copyright (c) 2001 Association of Mizar Users

MML identifier: ROBBINS1
[ MML identifier index ]


environ

 vocabulary LATTICES, BINOP_1, BOOLE, MIDSP_1, VECTSP_2, REALSET1, SUBSET_1,
      FUNCT_1, ARYTM_3, ARYTM_1, MIDSP_2, ROBBINS1;
 notation TARSKI, XBOOLE_0, REALSET1, STRUCT_0, LATTICES, VECTSP_2, BINOP_1,
      FUNCT_1, FUNCT_2, MIDSP_1;
 constructors VECTSP_2, BINOP_1, LATTICES, REALSET1, MIDSP_2, PARTFUN1;
 clusters STRUCT_0, RELSET_1, LATTICES, TEX_2, LATTICE2;
 definitions LATTICES;
 theorems STRUCT_0, LATTICES, REALSET1, BINOP_1;
 schemes BINOP_1;

begin :: Preliminaries

definition
 struct (1-sorted) ComplStr
     (# carrier -> set,
          Compl -> UnOp of the carrier #);
end;

definition
 struct(\/-SemiLattStr, ComplStr) ComplLattStr
     (# carrier -> set,
         L_join -> BinOp of the carrier,
          Compl -> UnOp of the carrier #);
end;

definition
  struct (ComplLattStr, LattStr) OrthoLattStr
     (# carrier -> set,
        L_join, L_meet -> BinOp of the carrier,
        Compl -> UnOp of the carrier #);
end;

definition
  func TrivComplLat -> strict ComplLattStr equals :Def1:
    ComplLattStr (# {{}}, op2, op1 #);
  coherence;
end;

definition
  func TrivOrtLat -> strict OrthoLattStr equals :Def2:
    OrthoLattStr (# {{}}, op2, op2, op1 #);
  coherence;
end;

definition
  cluster TrivComplLat -> non empty trivial;
  coherence by Def1,REALSET1:def 13,STRUCT_0:def 1;

  cluster TrivOrtLat -> non empty trivial;
  coherence by Def2,REALSET1:def 13,STRUCT_0:def 1;
end;

definition
  cluster strict non empty trivial OrthoLattStr;
  existence
  proof
    take TrivOrtLat;
    thus thesis;
  end;

  cluster strict non empty trivial ComplLattStr;
  existence
  proof
    take TrivComplLat;
    thus thesis;
  end;
end;

definition let L be non empty trivial ComplLattStr;
  cluster the ComplStr of L -> non empty trivial;
  coherence
  proof
      the carrier of the ComplStr of L is trivial by REALSET1:def 13;
    hence thesis by REALSET1:def 13,STRUCT_0:def 1;
  end;
end;

definition
  cluster strict non empty trivial 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;
 func x` -> Element of L equals :Def3:
   (the Compl of L).x;
 coherence;
end;

definition let L be non empty ComplLattStr,
               x,y be Element of L;
  redefine func x "\/" y;
  synonym x + y;
end;

definition let L be non empty ComplLattStr;
 let x,y be Element of L;
 func x *' y -> Element of L equals
:Def4: (x` "\/" y`)`;
 coherence;
end;

definition let L be non empty ComplLattStr;
  attr L is Robbins means :Def5:
   for x, y being Element of L holds
     ((x + y)` + (x + y`)`)` = x;

  attr L is Huntington means :Def6:
   for x, y being Element of L holds
     (x` + y`)` + (x` + y)` = x;
end;

definition let G be non empty \/-SemiLattStr;
  attr G is join-idempotent means :Def7:
   for x being Element of G holds
       x "\/" x = x;
end;

definition
  cluster TrivComplLat -> join-commutative join-associative Robbins
    Huntington join-idempotent;
  coherence
  proof
    set L = TrivComplLat;
    thus for x, y being Element of L holds
      x + y = y + x by REALSET1:def 20;
    thus for x, y, z being Element of L holds
      x + y + z = x + (y + z) by REALSET1:def 20;
    thus for x, y be Element of L holds
      ((x + y)` + (x + y`)`)` = x by REALSET1:def 20;
    thus for x, y being Element of L holds
      (x` + y`)` + (x` + y)` = x by REALSET1:def 20;
    let x be Element of L;
    thus thesis by REALSET1:def 20;
  end;

  cluster TrivOrtLat -> join-commutative join-associative Huntington Robbins;
  coherence
  proof
    set L = TrivOrtLat;
    thus for x, y being Element of L holds
      x + y = y + x by REALSET1:def 20;
    thus for x, y, z being Element of L holds
      x + y + z = x + (y + z) by REALSET1:def 20;
    thus for x, y being Element of L holds
      (x` + y`)` + (x` + y)` = x by REALSET1:def 20;
    let x, y be Element of L;
    thus thesis by REALSET1:def 20;
  end;
end;

definition
  cluster TrivOrtLat -> meet-commutative meet-associative
                        meet-absorbing join-absorbing;
  coherence
  proof
    set L = TrivOrtLat;
    thus for x, y being Element of L holds
      x "/\" y = y "/\" x by REALSET1:def 20;
    thus for x, y, z being Element of L holds
      x "/\" y "/\" z = x "/\" (y "/\" z) by REALSET1:def 20;
    thus for x, y being Element of L holds
      (x "/\" y) "\/" y = y by REALSET1:def 20;
    let x, y be Element of L;
    thus x "/\" (x "\/" y) = x by REALSET1:def 20;
  end;
end;

definition
 cluster strict join-associative join-commutative Robbins
   join-idempotent Huntington (non empty ComplLattStr);
 existence
 proof
   take TrivComplLat;
   thus thesis;
 end;
end;

definition
  cluster strict Lattice-like Robbins Huntington (non empty OrthoLattStr);
  existence
  proof
    take TrivOrtLat;
    thus thesis;
  end;
end;

definition let L be join-commutative (non empty ComplLattStr),
               x,y be Element of L;
  redefine func x + y;
  commutativity by LATTICES:def 4;
end;

theorem Th1: :: 4.8
  for L being Huntington join-commutative join-associative
    (non empty ComplLattStr),
      a, b being Element of L holds
  (a *' b) + (a *' b`) = a
proof
  let L be Huntington join-commutative join-associative
    (non empty ComplLattStr),
      a, b be Element of L;
  thus (a *' b) + (a *' b`) = (a` + b`)` + (a *' b`) by Def4
       .= (a` + b`)` + (a` + b``)` by Def4
       .= a by Def6;
end;

theorem Th2: :: 4.9
  for L being Huntington join-commutative join-associative
    (non empty ComplLattStr),
      a being Element of L holds
  a + a` = a` + a``
  proof
    let L be Huntington join-commutative join-associative
      (non empty ComplLattStr),
        a be Element of L;
    set y = a`, z = y``;
A1:  a = ((a` + y``)` + (a` + y`)`) by Def6;
      a` = ((a`` + a```)` + (a`` + a``)`) by Def6;
then a + a`
     = (y + z)` + (y + y`)` + (y` + y`)` + (y` + z)` by A1,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 Th3: :: 4.10
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      x being Element of L holds
    x`` = x
  proof
    let L be join-commutative join-associative Huntington
      (non empty ComplLattStr),
        x be Element of L;
    set y = x`;
A1:  (y`` + y`)` + (y`` + y)` = y` by Def6;
      (y + y``)` + (y + y`)` = x by Def6;
    hence thesis by A1,Th2;
  end;

theorem Th4: :: 4.11 revised p. 557 without idempotency
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b being Element of L holds
    a + a` = b + b`
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      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 Th5: :: 4.12
  for L being join-commutative join-associative join-idempotent Huntington
    (non empty ComplLattStr)
  ex c being Element of L st
   for a being Element of L holds c + a = c & a + a` = c
proof
  let L be join-commutative join-associative join-idempotent Huntington
    (non empty ComplLattStr);
  consider b be 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 Th6: :: 4.12
  for L being join-commutative join-associative join-idempotent Huntington
    (non empty ComplLattStr) holds
   L is upper-bounded
proof
  let L be join-commutative join-associative join-idempotent Huntington
    (non empty ComplLattStr);
  consider c being Element of L such that
A1:for a being Element of L holds c + a = c & a + a` = c
     by Th5;
    for a being Element of L holds a + c = c & a + a` = c
     by A1;
  hence thesis by A1,LATTICES:def 14;
end;

definition
  cluster join-commutative join-associative join-idempotent Huntington
    -> upper-bounded (non empty ComplLattStr);
  coherence by Th6;
end;

definition let L be join-commutative join-associative join-idempotent
  Huntington (non empty ComplLattStr);
  redefine func Top L means :Def8:
   ex a being Element of L st
    it = a + a`;
  compatibility
  proof
    let IT be Element of L;
    hereby assume A1: IT = Top L;
      consider a being Element of L;
      take a;
        for b being 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 being Element of L such that A2: IT = a + a`;
A3:  for b being 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 being Element of L holds b + (a + a`) = a + a`;
    hence IT = Top L by A2,A3,LATTICES:def 17;
  end;
end;

theorem Th7: :: 4.13
  for L being join-commutative join-associative join-idempotent Huntington
    (non empty ComplLattStr)
  ex c being Element of L st
   for a being Element of L holds c *' a = c & (a + a`)` = c
proof
  let L be join-commutative join-associative join-idempotent Huntington
    (non empty ComplLattStr);
  consider b be Element of L;
  take c = (b` + b)`;
  let a be Element of L;
  thus c *' a = ((b` + b)`` + a`)` by Def4
             .= ((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;

theorem Th8: :: 4.18
  for L being join-commutative join-associative (non empty ComplLattStr),
      a, b being Element of L holds
    a *' b = b *' a
proof
  let L be join-commutative join-associative (non empty ComplLattStr),
      a, b be Element of L;
  thus a *' b = (a` + b`)` by Def4
        .= b *' a by Def4;
end;

definition let L be join-commutative join-associative (non empty ComplLattStr);
 let x,y be Element of L;
 redefine func x *' y;
 commutativity by Th8;
end;

definition let L be join-commutative join-associative join-idempotent
    Huntington (non empty ComplLattStr);
  func Bot L -> Element of L means :Def9:
   for a being Element of L holds it *' a = it;
  existence
  proof
   consider c being Element of L such that
A1:  for a being Element of L holds c *' a = c & (a + a`)` = c
      by Th7;
   thus thesis by A1;
  end;
  uniqueness
    proof
     let c1,c2 be Element of L such that
A2:    for a being Element of L holds c1 *' a = c1 and
A3:    for a being Element of L holds c2 *' a = c2;
     thus c1 = c2 *' c1 by A2
            .= c2 by A3;
    end;
end;

theorem Th9:
  for L being join-commutative join-associative join-idempotent Huntington
    (non empty ComplLattStr),
      a being Element of L holds
  Bot L = (a + a`)`
proof
  let L be join-commutative join-associative join-idempotent Huntington
    (non empty ComplLattStr),
      a be Element of L;
    for b being 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 Def4
                  .= ((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 Th10:
  for L being join-commutative join-associative join-idempotent Huntington
    (non empty ComplLattStr) holds
  (Top L)` = Bot L & Top L = (Bot L)`
proof
  let L be join-commutative join-associative join-idempotent Huntington
    (non empty ComplLattStr);
  consider a be Element of L;
  thus (Top L)` = (a + a`)` by Def8
               .= Bot L by Th9;
  hence Top L = (Bot L)` by Th3;
end;

theorem Th11: :: 4.14
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b being Element of L st
    a` = b` holds a = b
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b being Element of L;
  assume A1: a` = b`;
  thus a = a`` by Th3 .= b by A1,Th3;
end;

theorem Th12: :: 4.15 proof without join-idempotency, no top at all
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b being Element of L holds
    a + (b + b`)` = a
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      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;
 O = O + O` by Th4
        .= O + O` + (O + O)` by A2,LATTICES:def 5
        .= O + (O + O)` by Th4;
then A3:O + O = O + O + (O + O)` by LATTICES:def 5
       .= O by Th4;
A4:O = a` + a 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,A3,A4,LATTICES:def 5
              .= a by A2,A3,A4,Def6;
end;

theorem Th13: :: 4.5
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a being Element of L holds
    a + a = a
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a be Element of L;
A1:(a + a)` = (a`` + a`)` + (a + a)` by Th12
          .= (a`` + a`)` + (a`` + a)` by Th3
          .= a` by Def6;
  thus a + a = (a + a)`` by Th3
            .= a by A1,Th3;
end;

definition
  cluster join-commutative join-associative Huntington ->
    join-idempotent (non empty ComplLattStr);
  coherence
  proof
    let L be non empty ComplLattStr;
    assume L is join-commutative join-associative Huntington;
    then for a being Element of L holds a + a = a by Th13;
    hence thesis by Def7;
  end;
end;

theorem Th14: :: 4.15
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a being Element of L holds
    a + Bot L = a
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      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 Th9;
end;

theorem :: 4.16
    for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a being Element of L holds
    a *' Top L = a
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a be Element of L;
    a *' Top L = (a` + (Top L)`)` by Def4
            .= (a` + Bot L)` by Th10
            .= a`` by Th14
            .= a by Th3;
  hence thesis;
end;

theorem Th16: :: 4.17
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a being Element of L holds
    a *' a` = Bot L
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a be Element of L;
  thus a *' a` = (a` + a``)` by Def4
              .= (Top L)` by Def8
              .= Bot L by Th10;
end;

theorem Th17: :: 4.19
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c being Element of L holds
    a *' (b *' c) = a *' b *' c
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c be Element of L;
  thus a *' b *' c = (a` + b`)` *' c by Def4
                  .= ((a` + b`)`` + c`)` by Def4
                  .= (a` + b` + c`)` by Th3
                  .= (a` + (b` + c`))` by LATTICES:def 5
                  .= (a` + (b` + c`)``)` by Th3
                  .= (a` + (b *' c)`)` by Def4
                  .= a *' (b *' c) by Def4;
end;

theorem Th18: :: 4.20
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b being Element of L holds
    a + b = (a` *' b`)`
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b be Element of L;
    a` *' b` = (a`` + b``)` by Def4
          .= (a`` + b)` by Th3
          .= (a + b)` by Th3;
  hence (a` *' b`)` = a + b by Th3;
end;

theorem :: 4.21
    for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a being Element of L holds
    a *' a = a
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a be Element of L;
  thus a *' a = (a` + a`)` by Def4
             .= a`` by Def7
             .= a by Th3;
end;

theorem :: 4.22
    for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a being Element of L holds
    a + Top L = Top L
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      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 Th21: :: 4.24
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b being Element of L holds
    a + (a *' b) = a
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a,b be Element of L;
  thus a + (a *' b) = (a *' b) + ((a *' b) + (a *' b`)) by Th1
                  .= (a *' b) + (a *' b) + (a *' b`) by LATTICES:def 5
                  .= (a *' b) + (a *' b`) by Def7
                  .= a by Th1;
end;

theorem Th22: :: 4.25
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b being Element of L holds
    a *' (a + b) = a
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a,b be Element of L;
  thus a *' (a + b) = (a` + (a + b)`)` by Def4
                  .= (a` + (a` *' b`)``)` by Th18
                  .= (a` + (a` *' b`))` by Th3
                  .= a`` by Th21
                  .= a by Th3;
end;

theorem Th23: :: 4.26
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b being 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 ComplLattStr),
      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 Th24: :: 4.27
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b being 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 ComplLattStr),
      a, b be Element of L;
  assume a + b = Top L;
then A1: a`` + b = Top L by Th3;
  assume a *' b = Bot L;
then A2:(a` + b`)` = Bot L by Def4;
    b` + a` = (a` + b`)`` by Th3
         .= Top L by A2,Th10;
  hence thesis by A1,Th23;
end;

theorem Th25: :: 4.28
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c being 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 ComplLattStr),
      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 Th1
    .= (a *' b) + (C + D) + E + F + G + H by LATTICES:def 5
    .= (a *' b) + (a *' b`) + E + F + G + H by Th1
    .= (a *' b) + (a *' b`) + (E + F) + G + H by LATTICES:def 5
    .= (a *' b) + (a *' b`) + (a` *' b) + G + H by Th1
    .= (a *' b) + (a *' b`) + (a` *' b) + (G + H) by LATTICES:def 5
    .= (a *' b) + (a *' b`) + (a` *' b) + (a` *' b`) by Th1
    .= a + (a` *' b) + (a` *' b`) by Th1
    .= a + ((a` *' b) + (a` *' b`)) by LATTICES:def 5
    .= a + a` by Th1;
  hence thesis by Def8;
end;

theorem Th26: :: 4.29
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c being 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 &
  (a *' b` *' c) *' (a` *' b *' c) = Bot L
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c be Element of L;
  A1: for a, b, c being 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 Th17
         .= a *' (c *' c`) *' b by Th17
         .= a *' Bot L *' b by Th16
         .= 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 Th17
    .= b *' c *' a *' (a` *' b) *' c by Th17
    .= b *' c *' a *' a` *' b *' c by Th17
    .= b *' c *' (a *' a`) *' b *' c by Th17
    .= b *' c *' (a *' a`) *' (b *' c) by Th17
    .= b *' c *' Bot L *' (b *' c) by Th16
    .= Bot L *' (b *' c) by Def9
    .= Bot L by Def9;
  thus (a *' b` *' c) *' (a` *' b *' c) = a *' (b` *' c) *' (a` *' b *'
 c) by Th17
     .= (b` *' c) *' a *' (a` *' (b *' c)) by Th17
     .= (b` *' c) *' a *' a` *' (b *' c) by Th17
     .= (b` *' c) *' (a *' a`) *' (b *' c) by Th17
     .= (b` *' c) *' Bot L *' (b *' c) by Th16
     .= Bot L *' (b *' c) by Def9
     .= Bot L by Def9;
  thus (a *' b *' c) *' (a` *' b` *' c) = (a *' (b *' c)) *' (a` *' b` *' c)
     by Th17
     .= (a *' (b *' c)) *' (a` *' (b` *' c)) by Th17
     .= Bot L by A1;
  thus (a *' b *' c`) *' (a` *' b` *' c`)
      = (a *' (b *' c`)) *' (a` *' b` *' c`) by Th17
     .= (a *' (b *' c`)) *' (a` *' (b` *' c`)) by Th17
     .= Bot L by A1;
  thus (a *' b` *' c) *' (a` *' b *' c)
      = (a *' (b` *' c)) *' (a` *' b *' c) by Th17
     .= (a *' (b` *' c)) *' (a` *' (b *' c)) by Th17
     .= Bot L by A1;
end;

theorem Th27: :: 4.30
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c being 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 ComplLattStr),
      a, b, c be Element of L;
  set A = a *' b *' c;
    a *' c = (a *' c *' b) + (a *' c *' b`) by Th1
        .= A + (a *' c *' b`) by Th17
        .= A + (a *' b` *' c) by Th17;
  hence (a *' b) + (a *' c) = A + (a *' b *' c`) +
    (A + (a *' b` *' c)) by Th1
    .= 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 Th28: :: 4.31
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c being 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 ComplLattStr),
      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 *' (b + c))` = (a` + (b + c)`)`` by Def4
                 .= a` + (b + c)` by Th3
                 .= a` + (b` *' c`)`` by Th18
                 .= a` + (b` *' c`) by Th3;
A2:a` = (a` *' b) + (a` *' b`) by Th1
    .= E + F + (a` *' b`) by Th1
    .= E + F + (G + H) by Th1;
 b` *' c` = (a *' (b` *' c`)) + (a` *' (b` *' c`)) by Th1
          .= D + (a` *' (b` *' c`)) by Th17
          .= D + H by Th17;
  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 Th29: :: 4.32
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c being Element of L holds
    ((a *' b) + (a *' c)) + (a *' (b + c))` = Top L
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      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;
A1:(a *' (b + c))` = D + E + F + G + H by Th28;
    (a *' b) + (a *' c) = ABC by Th27;
  then (a *' b) + (a *' c) + (a *' (b + c))` =
       ABC + (D + E + F + GH) by A1,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 Th25;
  hence thesis;
end;

theorem Th30:  :: 4.33
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c being Element of L holds
    ((a *' b) + (a *' c)) *' (a *' (b + c))` = Bot L
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      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;
A1: C *' D = Bot L by Th26;
A2: A *' G = Bot L & B *' H = Bot L & C *' E = Bot L by Th26;
A3:(a *' (b + c))` = DEFG + H by Th28;
 (A *' D) + (A *' E) = Bot L + (A *' E) by Th26
                     .= Bot L + Bot L by Th26
                     .= Bot L by Def7;
  then Top L = Bot L + (A *' (D + E))` by Th29
       .= (A *' (D + E))` by Th14;
  then Bot L = (A *' (D + E))`` by Th10
          .= A *' (D + E) by Th3;
  then (A *' (D + E)) + (A *' F) = Bot L + Bot L by Th26
                        .= Bot L by Def7;
  then Top L = Bot L + (A *' (D + E + F))` by Th29
       .= (A *' (D + E + F))` by Th14;
  then Bot L = (A *' (D + E + F))`` by Th10
          .= A *' (D + E + F) by Th3;
  then (A *' (D + E + F)) + (A *' G) = Bot L by A2,Def7;
  then Top L = Bot L + (A *' DEFG)` by Th29
       .= (A *' DEFG)` by Th14;
  then Bot L = (A *' DEFG)`` by Th10
          .= A *' DEFG by Th3;
then A4:(A *' DEFG) + (A *' H) = Bot L + Bot L by Th26
                        .= Bot L by Def7;
    (B *' D) + (B *' E) = Bot L + (B *' E) by Th26
                     .= Bot L + Bot L by Th26
                     .= Bot L by Def7;
  then Top L = Bot L + (B *' (D + E))` by Th29
       .= (B *' (D + E))` by Th14;
  then Bot L = (B *' (D + E))`` by Th10
          .= B *' (D + E) by Th3;
  then (B *' (D + E)) + (B *' F) = Bot L + Bot L by Th26
                           .= Bot L by Def7;
  then Top L = Bot L + (B *' (D + E + F))` by Th29
       .= (B *' (D + E + F))` by Th14;
  then Bot L = (B *' (D + E + F))`` by Th10
          .= B *' (D + E + F) by Th3;
  then (B *' (D + E + F)) + (B *' G) = Bot L + Bot L by Th26
                        .= Bot L by Def7;
  then Top L = Bot L + (B *' DEFG)` by Th29
       .= (B *' DEFG)` by Th14;
  then Bot L = (B *' DEFG)`` by Th10
          .= B *' DEFG by Th3;
then A5:(B *' DEFG) + (B *' H) = Bot L by A2,Def7;
A6:Top L = Bot L + (A *' (DEFG + H))` by A4,Th29
       .= (A *' (DEFG + H))` by Th14;
A7:Top L = Bot L + (B *' (DEFG + H))` by A5,Th29
       .= (B *' (DEFG + H))` by Th14;
    (C *' D) + (C *' E) = Bot L + Bot L by A1,Th26
                     .= Bot L by Def7;
  then Top L = Bot L + (C *' (D + E))` by Th29
       .= (C *' (D + E))` by Th14;
  then Bot L = (C *' (D + E))`` by Th10
          .= C *' (D + E) by Th3;
  then (C *' (D + E)) + (C *' F) = Bot L + Bot L by Th26
                        .= Bot L by Def7;
  then Top L = Bot L + (C *' (D + E + F))` by Th29
       .= (C *' (D + E + F))` by Th14;
  then Bot L = (C *' (D + E + F))`` by Th10
          .= C *' (D + E + F) by Th3;
  then (C *' (D + E + F)) + (C *' G) = Bot L + Bot L by Th26
                        .= Bot L by Def7;
  then Top L = Bot L + (C *' DEFG)` by Th29
       .= (C *' DEFG)` by Th14;
  then Bot L = (C *' DEFG)`` by Th10
          .= C *' DEFG by Th3;
  then (C *' DEFG) + (C *' H) = Bot L + Bot L by Th26
                        .= Bot L by Def7;
then A8:Top L = Bot L + (C *' (DEFG + H))` by Th29
        .= (C *' (DEFG + H))` by Th14;
A9: A *' (DEFG + H) = (A *' (DEFG + H))`` by Th3
                   .= Bot L by A6,Th10;
A10: B *' (DEFG + H) = (B *' (DEFG + H))`` by Th3
                   .= Bot L by A7,Th10;
A11: C *' (DEFG + H) = (C *' (DEFG + H))`` by Th3
                   .= Bot L by A8,Th10;
    (A *' (DEFG + H)) + (B *' (DEFG + H))
                    = Bot L by A9,A10,Def7;
  then Top L = Bot L + ((A + B) *' (DEFG + H))` by Th29
       .= ((A + B) *' (DEFG + H))` by Th14;
  then Bot L = ((A + B) *' (DEFG + H))`` by Th10
          .= (A + B) *' (DEFG + H) by Th3;
  then ((A + B) *' (DEFG + H)) + (C *' (DEFG + H))
      = Bot L by A11,Def7;
  then Top L = Bot L + ((A + B + C) *' (DEFG + H))` by Th29
       .= ((A + B + C) *' (DEFG + H))` by Th14;
  then Bot L = ((A + B + C) *' (DEFG + H))`` by Th10
          .= (A + B + C) *' (DEFG + H) by Th3;
  hence thesis by A3,Th27;
end;

theorem Th31: :: 4.34
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c being Element of L holds
    a *' (b + c) = (a *' b) + (a *' c)
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c be Element of L;
A1:(a *' b) + (a *' c) + (a *' (b + c))` = Top L by Th29;
    ((a *' b) + (a *' c)) *' (a *' (b + c))` = Bot L by Th30;
  then ((a *' b) + (a *' c))` = (a *' (b + c))` by A1,Th24;
  hence thesis by Th11;
end;

theorem :: 4.35
    for L being join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c being Element of L holds
    a + (b *' c) = (a + b) *' (a + c)
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr),
      a, b, c be Element of L;
  thus a + (b *' c) = a + (b` + c`)` by Def4
              .= (a` *' (b` + c`)``)` by Th18
              .= (a` *' (b` + c`))` by Th3
              .= ((a` *' b`) + (a` *' c`))` by Th31
              .= ((a` *' b`)` *' (a` *' c`)`)`` by Th18
              .= (a` *' b`)` *' (a` *' c`)` by Th3
              .= (a + b) *' (a` *' c`)` by Th18
              .= (a + b) *' (a + c) by Th18;
end;

begin :: Pre-Ortholattices

definition let L be non empty OrthoLattStr;
  attr L is well-complemented means :Def10:
    for a being Element of L holds
     a` is_a_complement_of a;
end;

definition
  cluster TrivOrtLat -> Boolean well-complemented;
  coherence
  proof
    set L = TrivOrtLat;
    thus L is lower-bounded
    proof
      consider c being Element of L;
      take c;
      thus thesis by REALSET1:def 20;
    end;
    thus L is upper-bounded;
    thus L is complemented
    proof
      let b be Element of L;
      take a = b;
        a is_a_complement_of b
      proof
        thus a "\/" b = Top L & b "\/" a = Top L &
             a "/\" b = Bottom L & b "/\" a = Bottom L by REALSET1:def 20;
      end;
      hence thesis;
    end;
    thus L is distributive
    proof
      let x, y, z be Element of L;
      thus thesis by REALSET1:def 20;
    end;
    thus L is well-complemented
    proof
      let a be Element of L;
      thus a` is_a_complement_of a
      proof
        thus a` "\/" a = Top L & a "\/" a` = Top L &
             a` "/\" a = Bottom L & a "/\" a` = Bottom L by REALSET1:def 20;
      end;
    end;
  end;
end;

definition
  mode preOrthoLattice is Lattice-like (non empty OrthoLattStr);
end;

definition
  cluster strict Boolean well-complemented preOrthoLattice;
  existence
  proof
    take TrivOrtLat;
    thus thesis;
  end;
end;

theorem Th33:
  for L being distributive well-complemented preOrthoLattice,
      x being Element of L
     holds x`` = x
  proof
    let L be distributive well-complemented preOrthoLattice;
    let x be Element of L;
A1:  x` is_a_complement_of x by Def10;
      x`` is_a_complement_of x` by Def10;
then A2:  x`` + x` = Top L & x`` "/\" x` = Bottom L by LATTICES:def 18;
      x` "\/" x = Top L & x` "/\" x = Bottom L by A1,LATTICES:def 18;
    hence thesis by A2,LATTICES:32;
  end;

theorem Th34:
  for L being bounded distributive well-complemented preOrthoLattice,
      x, y being Element of L
     holds x "/\" y = (x` "\/" y`)`
  proof
    let L be bounded distributive well-complemented preOrthoLattice;
    let x, y be Element of L;
      x` is_a_complement_of x by Def10;
then A1:  x` "\/" x = Top L & x` "/\" x = Bottom L by LATTICES:def 18;
      y` is_a_complement_of y by Def10;
then A2:  y` "\/" y = Top L & y` "/\" y = Bottom L by LATTICES:def 18;
A3: (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 A1,LATTICES:def 7
       .= Bottom L "\/" (x "/\" Bottom L) by A2,LATTICES:40
       .= Bottom L "\/" Bottom L by LATTICES:40
       .= Bottom L by LATTICES:39;
A4:  x` "\/" Top L = Top L "\/" x` by LATTICES:def 4 .= Top L by LATTICES:44;
A5:  y` "\/" Top L = Top L "\/" y` by LATTICES:def 4 .= Top L by LATTICES:44;
A6: (x` "\/" y`) "\/" (x "/\" y) = (x` "\/" y` "\/" x) "/\" (x` "\/" y` "\/" y)
       by LATTICES:31
       .= (y` "\/" x` "\/" x) "/\" (x` "\/" y` "\/" y) by LATTICES:def 4
       .= (y` "\/" x` "\/" x) "/\" Top L by A2,A4,LATTICES:def 5
       .= Top L "/\" Top L by A1,A5,LATTICES:def 5
       .= Top L by LATTICES:43;
    A7: (x "/\" y)` is_a_complement_of (x "/\" y) by Def10;
then A8:  (x "/\" y)` "\/" (x "/\" y) = Top L & (x "/\" y)` "/\" (x "/\" y) =
Bottom L
       by LATTICES:def 18;
      (x "/\" y) + (x "/\" y)` = (x "/\" y) + (x` + y`) by A6,A7,LATTICES:def
18
;
    then (x "/\" y)` = x` "\/" y` by A3,A8,LATTICES:32;
    hence thesis by Th33;
  end;

begin :: Correspondence between boolean preOrthoLattice and boolean lattice
      :: according to the definition given in \cite{LATTICES.ABS}

definition let L be non empty ComplLattStr;
  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 being 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 being BinOp of the carrier of L such that
A1:  for a, b being Element of L holds
      K.(a,b) = F(a,b) from BinOpLambda;
    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 &
    the L_join of L1 = the L_join of L &
    the Compl of L1 = the Compl of L &
    for a, b being Element of L holds
      (the L_meet of L1).(a,b) = a *' b and
A3: the carrier of L2 = the carrier of L &
    the L_join of L2 = the L_join of L &
    the Compl of L2 = the Compl of L &
    for a, b being 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,A3;
      now let a, b be Element of L;
      thus A.(a,b) = a *' b by A2
                  .= B.(a,b) by A3;
    end;
    hence thesis by A2,A3,BINOP_1:2;
  end;
end;

definition let L be non empty ComplLattStr;
  cluster CLatt L -> non empty;
  coherence
  proof
      the carrier of CLatt L = the carrier of L by Def11;
    hence thesis by STRUCT_0:def 1;
  end;
end;

definition let L be join-commutative (non empty ComplLattStr);
  cluster CLatt L -> join-commutative;
  coherence
  proof
    let a,b be Element of CLatt L;
A1:  the carrier of L = the carrier of CLatt L by Def11;
    the L_join of L = the L_join of CLatt L by Def11;
    hence a "\/" b = (the L_join of L).(a,b) by LATTICES:def 1
                .= (the L_join of L).(b,a) by A1,BINOP_1:def 2
                .= (the L_join of CLatt L).(b,a) by Def11
                .= b "\/" a by LATTICES:def 1;
  end;
end;

definition let L be join-associative (non empty ComplLattStr);
  cluster CLatt L -> join-associative;
  coherence
  proof
    let a, b, c be Element of CLatt L;
    set K = the L_join of L, M = the L_join of CLatt L;
A1:  the carrier of L = the carrier of CLatt L by Def11;
A2:  K = M by Def11;
    thus (a "\/" b) "\/" c = M.(a "\/" b,c) by LATTICES:def 1
                  .= M.(M.(a,b),c) by LATTICES:def 1
                  .= K.(a,K.(b,c)) by A1,A2,BINOP_1:def 3
                  .= M.(a,b "\/" c) by A2,LATTICES:def 1
                  .= a "\/" (b "\/" c) by LATTICES:def 1;
  end;
end;

definition let L be join-commutative join-associative (non empty ComplLattStr);
  cluster CLatt L -> meet-commutative;
  coherence
  proof
    let a, b be Element of CLatt L;
    reconsider a' = a, b' = b as Element of L by Def11;
    thus a "/\" b = (the L_meet of CLatt L).(a,b) by LATTICES:def 2
               .= b' *' a' by Def11
               .= (the L_meet of CLatt L).(b,a) by Def11
               .= b "/\" a by LATTICES:def 2;
  end;
end;

theorem Th35:
  for L being non empty ComplLattStr,
      a, b being Element of L,
      a', b' being Element of CLatt L st
   a = a' & b = b' holds a *' b = a' "/\" b' & a + b = a' "\/" b' & a` = a'`
proof
  let L be non empty ComplLattStr,
      a, b be Element of L,
      a', b' be Element of CLatt L;
  assume A1: a = a' & b = b';
  thus a *' b = (the L_meet of CLatt L).(a,b) by Def11
            .= a' "/\" b' by A1,LATTICES:def 2;
  thus a + b = (the L_join of L).(a,b) by LATTICES:def 1
            .= (the L_join of CLatt L).(a,b) by Def11
            .= a' "\/" b' by A1,LATTICES:def 1;
  thus a` = (the Compl of L).a by Def3
         .= (the Compl of CLatt L).a by Def11
         .= a'` by A1,Def3;
end;

definition let L be join-commutative join-associative Huntington
  (non empty ComplLattStr);
  cluster CLatt L -> meet-associative join-absorbing meet-absorbing;
  coherence
  proof
    hereby let a, b, c be Element of CLatt L;
      reconsider a' = a, b' = b, c' = c as Element of L
        by Def11;
A1:    a' *' b' = a "/\" b & b' *' c' = b "/\" c by Th35;
      hence a "/\" b "/\" c = a' *' b' *' c' by Th35
                      .= a' *' (b' *' c') by Th17
                      .= a "/\" (b "/\" c) by A1,Th35;
    end;
    hereby let a, b be Element of CLatt L;
      reconsider a' = a, b' = b as Element of L by Def11;
     a' + b' = a "\/" b by Th35;
      hence a "/\" (a "\/" b) = a' *' (a' + b') by Th35
                        .= a by Th22;
    end;
    let a, b be Element of CLatt L;
    reconsider a' = a, b' = b as Element of L by Def11;
   a' *' b' = a "/\" b by Th35;
    hence (a "/\" b) "\/" b = (a' *' b') + b' by Th35
                      .= b by Th21;
  end;
end;

definition let L be Huntington (non empty ComplLattStr);
  cluster CLatt L -> Huntington;
  coherence
  proof
    let x, y be Element of CLatt L;
    reconsider x' = x, y' = y as Element of L by Def11;
A1:  x` = x'` & y` = y'` by Th35;
    then x` + y` = x'` + y'` by Th35;
then A2:  (x` + y`)` = (x'` + y'`)` by Th35;
      x` + y = x'` + y' by A1,Th35;
    then (x` + y)` = (x'` + y')` by Th35;
    hence (x` + y`)` + (x` + y)` = (x'` + y'`)` + (x'` + y')` by A2,Th35
                                .= x by Def6;
  end;
end;

definition let L be join-commutative join-associative Huntington
  (non empty ComplLattStr);
  cluster CLatt L -> lower-bounded;
  coherence
  proof
    thus CLatt L is lower-bounded
    proof
      set c' = Bot L;
      reconsider c = c' as Element of CLatt L by Def11;
      take c;
      let a be Element of CLatt L;
      reconsider a' = a as Element of L by Def11;
      thus c "/\" a = c' *' a' by Th35 .= c by Def9;
      hence a "/\" c = c;
    end;
  end;
end;

theorem Th36:
  for L being join-commutative join-associative Huntington
    (non empty ComplLattStr) holds
   Bot L = Bottom CLatt L
proof
  let L be join-commutative join-associative Huntington
    (non empty ComplLattStr);
    the carrier of CLatt L = the carrier of L by Def11;
  then reconsider C = Bot L as Element of CLatt L;
    for a being Element of CLatt L holds C "/\" a = C & a "/\"
 C = C
  proof
    let a be Element of CLatt L;
    reconsider a' = a as Element of L by Def11;
    thus C "/\" a = Bot L *' a' by Th35
               .= C by Def9;
    hence thesis;
  end;
  hence thesis by LATTICES:def 16;
end;

definition let L be join-commutative join-associative Huntington
  (non empty ComplLattStr);
  cluster CLatt L -> complemented distributive bounded;
  coherence
  proof
A1:  the Compl of CLatt L = the Compl of L by Def11;
    thus CLatt L is complemented
    proof
      let b be Element of CLatt L;
      take a = b`;
      reconsider a' = a, b' = b as Element of L by Def11;
      thus a + b = Top CLatt L by Def8;
      thus b + a = Top CLatt L by Def8;
A2:    a'` = (the Compl of L).a' by Def3
         .= a` by A1,Def3
         .= b' by Th3;
      thus a "/\" b = a' *' b' by Th35
                 .= (a'` + b'`)` by Def4
                 .= Bot L by A2,Th9
                 .= Bottom CLatt L by Th36;
      hence b "/\" a = Bottom CLatt L;
    end;
    hereby let a, b, c be Element of CLatt L;
      reconsider a' = a, b' = b, c' = c as Element of L
        by Def11;
A3:    b' + c' = b "\/" c & a "/\" b = a' *' b' & a "/\" c = a' *' c' by Th35;
      hence a "/\" (b "\/" c) = a' *' (b' + c') by Th35
                        .= (a' *' b') + (a' *' c') by Th31
                        .= (a "/\" b) "\/" (a "/\" c) by A3,Th35;
    end;
    thus CLatt L is lower-bounded;
    thus CLatt L is upper-bounded;
  end;
end;

begin :: Proofs according to Bernd Ingo Dahn

definition let G be non empty ComplLattStr,
               x be Element of G;
  redefine func x`;
  synonym -x;
end;

definition let G be join-commutative (non empty ComplLattStr);
  redefine attr G is Huntington means :Def12:
   for x, y being Element of G holds
    -(-x + -y) + -(x + -y) = y;
  compatibility
  proof
    thus G is Huntington implies
      for x, y being Element of G holds
      -(-x + -y) + -(x + -y) = y by Def6;
    assume A1: for x, y being 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 ComplLattStr;
  attr G is with_idempotent_element means :Def13:
   ex x being Element of G st x + x = x;
  correctness;
end;

 reserve G for Robbins join-associative join-commutative
   (non empty ComplLattStr);
 reserve x, y, z, u, v for Element of G;

definition let G be non empty ComplLattStr,
               x, y be Element of G;
  func \delta (x, y) -> Element of G equals :Def14:
   -(-x + y);
  coherence;
end;

definition let G be non empty ComplLattStr,
               x, y be Element of G;
  func Expand (x, y) -> Element of G equals :Def15:
   \delta (x + y, \delta(x, y));
  coherence;
end;

definition let G be non empty ComplLattStr,
               x be Element of G;
  func x _0 -> Element of G equals :Def16:
   -(-x + x);
  coherence;

  func Double x -> Element of G equals :Def17:
    x + x;
  coherence;
end;

definition let G be non empty ComplLattStr,
               x be Element of G;
  func x _1 -> Element of G equals :Def18:
   x _0 + x;
  coherence;
  func x _2 -> Element of G equals :Def19:
   x _0 + Double x;
  coherence;
  func x _3 -> Element of G equals :Def20:
   x _0 + (Double x + x);
  coherence;
  func x _4 -> Element of G equals :Def21:
   x _0 + (Double x + Double x);
  coherence;
end;

theorem Th37:
  \delta ((x + y), (\delta (x, y))) = y
proof
  thus \delta ((x + y), (\delta (x, y))) = \delta (x + y, -(-x + y)) by Def14
         .= -(-(x + y) + -(-x + y)) by Def14
         .= y by Def5;
end;

theorem Th38:
  Expand (x, y) = y
proof
  thus Expand (x, y) = \delta (x + y, \delta(x, y)) by Def15
               .= y by Th37;
end;

theorem Th39:
  \delta (-x + y, z) = -(\delta (x, y) + z)
proof
  thus \delta (-x + y, z) = -(-(-x + y) + z) by Def14
                    .= -(\delta (x, y) + z) by Def14;
end;

theorem Th40:
  \delta (x, x) = x _0
proof
  thus \delta (x, x) = -(-x + x) by Def14
               .= x _0 by Def16;
end;

theorem Th41:
  \delta (Double x, x _0) = x
proof
  thus \delta (Double x, x _0) = \delta (Double x, \delta (x, x)) by Th40
                    .= \delta (x + x, \delta (x, x)) by Def17
                    .= Expand (x, x) by Def15
                    .= x by Th38;
end;

theorem Th42: :: Lemma 1
  \delta (x _2, x) = x _0
proof
  thus \delta (x _2, x) = \delta (Double x + x _0, x) by Def19
                  .= \delta (Double x + x _0, \delta (Double x, x _0)) by Th41
      .= Expand (Double x, x _0) by Def15
      .= x _0 by Th38;
end;

theorem Th43:
  x _2 + x = x _3
proof
  thus x _2 + x = x _0 + Double x + x by Def19
          .= x _0 + (Double x + x) by LATTICES:def 5
          .= x _3 by Def20;
end;

theorem Th44:
  x _4 + x _0 = x _3 + x _1
proof
  thus x _4 + x _0 = x _0 + (Double x + Double x) + x _0 by Def21
          .= (x _0 + Double x) + Double x + x _0 by LATTICES:def 5
          .= (x _0 + Double x) + (x + x) + x _0 by Def17
          .= (x _0 + Double x) + x + 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 Def20
          .= x _3 + (x + x _0) by LATTICES:def 5
          .= x _3 + x _1 by Def18;
end;

theorem Th45:
  x _3 + x _0 = x _2 + x _1
proof
  thus x _3 + x _0 = x _0 + (Double x + x) + x _0 by Def20
          .= (x _0 + Double x) + x + x _0 by LATTICES:def 5
          .= x _2 + x + x _0 by Def19
          .= x _2 + (x + x _0) by LATTICES:def 5
          .= x _2 + x _1 by Def18;
end;

theorem Th46:
  x _3 + x = x _4
proof
  thus x _3 + x = x _0 + (Double x + x) + x by Def20
          .= x _0 + (Double x + x + x) by LATTICES:def 5
          .= x _0 + (Double x + (x + x)) by LATTICES:def 5
          .= x _0 + (Double x + Double x) by Def17
          .= x _4 by Def21;
end;

theorem Th47: :: Lemma 2
  \delta (x _3, x _0) = x
proof
  thus x = Expand (x _2, x) by Th38
     .= \delta (x + x _2, \delta (x _2, x)) by Def15
     .= \delta (x + x _2, x _0) by Th42
     .= \delta (x _3, x _0) by Th43;
end;

theorem Th48:  :: Left Argument Substitution
  -x = -y implies \delta (x, z) = \delta (y,z)
proof
  assume A1: -x = -y;
  thus \delta (x, z) = -(-x + z) by Def14
               .= \delta (y,z) by A1,Def14;
end;

theorem Th49: :: Exchange
  \delta (x, -y) = \delta (y, -x)
proof
  thus \delta (x, -y) = -(-x + -y) by Def14
                .= \delta (y, -x) by Def14;
end;

theorem Th50: :: Lemma 3
  \delta (x _3, x) = x _0
proof
A1:  x = Expand (-x _3 + x _0, x) by Th38
   .= \delta (-x _3 + x _0 + x, \delta (-x _3 + x _0, x)) by Def15
   .= \delta (-x _3 + (x _0 + x), \delta (-x _3 + x _0, x)) by LATTICES:def 5
   .= \delta (-x _3 + x _1, \delta (-x _3 + x _0, x)) by Def18
   .= \delta (-x _3 + x _1, -(\delta (x _3, x _0) + x)) by Th39
   .= \delta (-x _3 + x _1, -(x + x)) by Th47
   .= \delta (-x _3 + x _1, -Double x) by Def17;
A2:  -Double x = Expand (-x _3 + x _1, -Double x) by Th38
     .= \delta (-x _3 + x _1 + -Double x, x) by A1,Def15;
  set alpha = -x _3 + x _1 + -Double x;
A3:-Double x = -(-alpha + x) by A2,Def14;
A4:x = \delta (Double x, x _0) by Th41 .= \delta (-alpha + x, x _0)
     by A3,Th48;
 -x _3 = Expand (x _1 + -Double x, -x _3) by Th38
  .= \delta (x _1 + -Double x + -x _3, \delta (x _1 + -Double x, -x _3))
      by Def15
  .= \delta (-x _3 + x _1 + -Double x, \delta (x _1 + -Double x, -x _3))
                   by LATTICES:def 5
  .= \delta (alpha, \delta (x _3, -(x _1 + -Double x))) by Th49
  .= \delta (alpha, \delta (x _3, \delta (Double x, x _1))) by Def14
  .= \delta (alpha, \delta (x _0 + (x + Double x), \delta (Double x, x _1)))
    by Def20
  .= \delta (alpha, \delta (x _0 + x + Double x, \delta (Double x, x _1)))
            by LATTICES:def 5
  .= \delta (alpha, \delta (Double x + x _1, \delta (Double x, x _1))) by Def18
  .= \delta (alpha, Expand (Double x, x _1)) by Def15
  .= \delta (alpha, x _1) by Th38
  .= -(-alpha + x _1) by Def14;
  hence \delta (x _3, x) = \delta (-alpha + x _1, x) by Th48
     .= \delta (-alpha + (x _0 + x), x) by Def18
     .= \delta (-alpha + x + x _0, \delta (-alpha + x, x _0))
                         by A4,LATTICES:def 5
     .= Expand (-alpha + x, x _0) by Def15
     .= x _0 by Th38;
end;

theorem Th51: :: Lemma 4
  \delta (x _1 + x _3, x) = x _0
proof
    x _0 = Expand (x _4, x _0) by Th38
      .= \delta (x _4 + x _0, \delta (x _4, x _0)) by Def15
      .= \delta (x _4 + x _0, \delta (x _4, \delta (x _3, x))) by Th50
      .= \delta (x _3 + x _1, \delta (x _4, \delta (x _3, x))) by Th44
      .= \delta (x _3 + x _1, \delta (x _3 + x, \delta (x _3, x))) by Th46
      .= \delta (x _3 + x _1, Expand (x _3, x)) by Def15
      .= \delta (x _3 + x _1, x) by Th38;
  hence thesis;
end;

theorem Th52: :: Lemma 5
  \delta (x _1 + x _2, x) = x _0
proof
  thus x _0 = Expand (x _3, x _0) by Th38
      .= \delta (x _3 + x _0, \delta(x _3, x _0)) by Def15
      .= \delta (x _1 + x _2, \delta(x _3, x _0)) by Th45
      .= \delta (x _1 + x _2, x) by Th47;
end;

theorem Th53: :: Lemma 6
  \delta (x _1 + x _3, x _0) = x
proof
  thus x = Expand (x _1 + x _2, x) by Th38
   .= \delta (x _1 + x _2 + x, \delta(x _1 + x _2, x)) by Def15
   .= \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 Th43
   .= \delta (x _1 + x _3, x _0) by Th52;
end;

definition let G, x;
  func \beta x -> Element of G equals :Def22:
   -(x _1 + x _3) + x + -(x _3);
  coherence;
end;

theorem Th54: :: Lemma 7
  \delta (\beta x, x) = -x _3
proof
  thus -x _3 =
  \delta (-(x _1 + x _3) + x + -(x _3), \delta (-(x _1 + x _3) + x, -(x _3)))
     by Th37
     .= \delta (\beta x, \delta (-(x _1 + x _3) + x, -(x _3))) by Def22
     .= \delta (\beta x, \delta (x _3, -(-(x _1 + x _3) + x))) by Th49
     .= \delta (\beta x, \delta (x _3, \delta (x _1 + x _3, x))) by Def14
     .= \delta (\beta x, \delta (x _3, x _0)) by Th51
     .= \delta (\beta x, x) by Th47;
end;

theorem Th55: :: Lemma 8
  \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 Th37
.=\delta (-(x _1 + x _3) + x + -(x _3), \delta (x + -(x _3), -(x _1 + x _3)))
     by LATTICES:def 5
  .= \delta (\beta x, \delta (x + -(x _3), -(x _1 + x _3))) by Def22
  .= \delta (\beta x, \delta (x _1 + x _3, -(x + -x _3))) by Th49
  .= \delta (\beta x, \delta (x _1 + x _3, \delta (x _3, x))) by Def14
  .= \delta (\beta x, \delta (x _1 + x _3, x _0)) by Th50
  .= \delta (\beta x, x) by Th53;
end;

theorem :: Winker Second Condition
    ex y, z st -(y + z) = -z
proof
  consider x;
  take y = x _1, z = x _3;
    -(y + z) = \delta (\beta x, x) by Th55
    .= -z by Th54;
  hence thesis;
end;

begin :: Proofs according to Bill McCune

theorem
    (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 Th58:
  G is with_idempotent_element implies G is Huntington
proof
  assume G is with_idempotent_element;
  then consider C being Element of G such that
A1: C + C = C by Def13;

  assume G is non Huntington;
  then consider B, A being Element of G such that
A2: -(-B + -A) + -(B + -A) <> A by Def12;

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

A4: 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;

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

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

     set D = C + -C + -C;

 -(-C + -(C + -C + -C))
          = -(-(-(C + -C + -C) + C) + -(C + C + (-C + -C)))
             by A1,A5,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 -(C + -C) = -(C + -C + -C) by A5,Def5;

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

A8:now let x;
      thus x = -(-(C + -(C + -C) + x) + -(-C + -(C + -C) + x)) by A3,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 A2;
end;

definition
  cluster TrivComplLat -> with_idempotent_element;
  coherence
  proof
    consider x be Element of TrivComplLat;
    take x;
    thus x = x + x by REALSET1:def 20;
  end;
end;

definition
  cluster with_idempotent_element ->
    Huntington (Robbins join-associative join-commutative
      (non empty ComplLattStr));
  coherence by Th58;
end;

theorem Th59:
  (ex c, d being Element of G st c + d = c) implies
    G is Huntington
proof
  given C, D being Element of G such that
A1: C + D = C;

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

A3: now let x, y;
     thus -(-(D + -(C + x) + y) + -(C + x + y))
        = -(-(-(C + x) + (D + y)) + -(C + D + x + y)) by A1,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;

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, 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;

A6: now let x;
       thus D = -(-(-(-x + C) + -(x + C) + D) + -(C + D)) by A4
        .= -(-C + -(D + -(C + -x) + -(C + x))) by A1,LATTICES:def 5;
     end;

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

A7:   -(D + -(C + -E)) = -E by A2,Def5;

 now
     thus -(L + -(C + L)) = -(-(D + -(C + L)) + -((D + C) + L)) by A1,A2,Def5
                    .= -(-(D + -(C + L)) + -(D + (C + L))) by LATTICES:def 5
                    .= D by Def5;
     end;

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

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

A9: C = -(-(D + -L + C) + -(-(D + -C) + C)) by A7,Def5
       .= -(-L + -(C + -L)) by A1,LATTICES:def 5;

A10: now let x, y, z;
         set k = -(-x + y);
           -(-(k + x + y) + y) = k by A5;
        hence z = -(-(-(-(-x + y) + x + y) + y + z) + -(-(-x + y) + z))
          by Def5;
       end;

A11: -(C + -(D + -C))
                = -(D + -(D + -(C + -(D + -C)) + -C)) by A8,LATTICES:def 5
               .= -C by A2,A7,Def5;

then A12: -(C + -(C + -(C + -C))) = -(C + -C) by A9,Def5;

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

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

then C = -(-(C + -C) + K) by A12,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 A9,A10,A11;

then D + -(C + -C)
       = -(-(D + -(C + C) + -(C + -C)) + -C) by A3
      .= -(-C + -(D + -(C + -C) + -(C + C))) by LATTICES:def 5
      .= D by A6;

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

A14: now let x;
      thus x = -(-(C + -(C + -C) + x) + -(-C + -(C + -C) + x)) by A9,A11,A13,
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;

  set e = -(C + -C);
    e = e + e by A14;
  then G is with_idempotent_element by Def13;
  hence thesis by Th58;
end;

theorem Th60:
  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 + (y + y)) + -(-x + y)) by LATTICES:def 5
         .= -(-(-(-x + y) + x + Double y) + -(-x + y)) by Def17;
     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;
      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;

A12: now let x;
A13:    -(-(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 + (x + x))) + x)
            by LATTICES:def 5
         .= -(-(-(-(Double x + x) + x) + (Double x + Double x)) + x)
            by Def17;
       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,A13;
     end;

A14: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 A12;
     end;

A15: now let x, y;
      thus
        Double x = -(-(-(-(Double x + x) + x) + -(Double x + x) + Double x) +
        -(x + Double x)) by A14
         .= -(-(Double x + x) + x) + Double x by A11;
      end;

  consider x;
  set c = Double x, d = -(-(Double x + x) + x);
  take d, c;
  thus thesis by A15;
end;

definition
 cluster Robbins -> Huntington (join-associative join-commutative
   (non empty ComplLattStr));
 coherence
 proof
   let K be join-associative join-commutative (non empty ComplLattStr);
   assume A1: K is Robbins;
   then consider y, z be Element of K such that
A2:   y + z = z by Th60;
   thus thesis by A1,A2,Th59;
 end;
end;

definition let L be non empty OrthoLattStr;
  attr L is de_Morgan means :Def23:
   for x, y being Element of L holds x "/\" y = (x` "\/" y`)`;
end;

definition let L be non empty ComplLattStr;
  cluster CLatt L -> de_Morgan;
  coherence
  proof
    let x, y be Element of CLatt L;
    reconsider x' = x, y' = y as Element of L by Def11;
      x'` = x` & y'` = y` by Th35;
    then x'` "\/" y'` = x` "\/" y` by Th35;
  then (x'` "\/" y'`)` = (x` "\/" y`)` by Th35;
    then (x` "\/" y`)` = x' *' y' by Def4;
    hence thesis by Th35;
  end;
end;

theorem Th61:
  for L being well-complemented join-commutative meet-commutative
    (non empty OrthoLattStr),
      x being 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 by LATTICES:def 18;
    thus thesis by A1,LATTICES:def 18;
  end;

theorem Th62:
  for L being bounded distributive well-complemented preOrthoLattice holds
    (Top L)` = Bottom L
  proof
    let L be bounded distributive well-complemented preOrthoLattice;
    consider x being Element of L;
      (Top L)` = (x`` + x`)` by Th61
         .= x` "/\" x by Th34
         .= Bottom L by Th61;
    hence thesis;
  end;

definition
  cluster TrivOrtLat -> de_Morgan;
  coherence
  proof
    let x, y be Element of TrivOrtLat;
    thus thesis by REALSET1:def 20;
  end;
end;

definition
  cluster strict de_Morgan Boolean Robbins Huntington preOrthoLattice;
  existence
  proof
    take TrivOrtLat;
    thus thesis;
  end;
end;

Lm1:
  for L being de_Morgan (non empty OrthoLattStr),
      a,b being Element of L holds
    a *' b = a "/\" b
  proof
    let L be de_Morgan (non empty OrthoLattStr),
        a,b be Element of L;
    thus a *' b = (a` "\/" b`)` by Def4
              .= a "/\" b by Def23;
  end;

definition
  cluster join-associative join-commutative de_Morgan ->
    meet-commutative (non empty OrthoLattStr);
  coherence
  proof
    let L be non empty OrthoLattStr;
    assume A1: L is join-associative join-commutative de_Morgan;
    let a,b be Element of L;
    thus a "/\" b = a *' b by A1,Lm1
               .= b *' a by A1,Th8
               .= b "/\" a by A1,Lm1;
  end;
end;

theorem Th63:
  for L being 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 being Element of L holds C "/\" a = C & a "/\" C = C
  proof
    let a be Element of L;
    reconsider a' = a as Element of L;
    thus C "/\" a = Bot L *' a' by Lm1
               .= C by Def9;
    hence thesis;
  end;
  then L is lower-bounded by LATTICES:def 13;
  hence thesis by A1,LATTICES:def 16;
end;

definition
  cluster Boolean -> Huntington (well-complemented preOrthoLattice);
  coherence
  proof
    let L be well-complemented preOrthoLattice;
    assume A1: L is Boolean;
then A2:  L is bounded distributive complemented by LATTICES:def 20;
    reconsider L' = L as Boolean preOrthoLattice by A1;
A3:  for x being Element of L' holds
      Top L' "/\" x = x by LATTICES:43;
      now let x, y be Element of L;
      thus (x` "\/" y`)` "\/" (x` "\/" y)` = (x "/\" y) + (x` + y)` by A2,Th34
              .= (x + (x` + y)`) "/\" (y + (x` + y)`) by A2,LATTICES:31
              .= (x + (x` + y``)`) "/\" (y + (x` + y)`) by A2,Th33
              .= (x + (x "/\" y`)) "/\" (y + (x` + y)`) by A2,Th34
              .= x "/\" (y + (x` + y)`) by LATTICES:def 8
              .= x "/\" (y + (x` + y``)`) by A2,Th33
              .= x "/\" (y + (x "/\" y`)) by A2,Th34
              .= x "/\" ((y + x) "/\" (y + y`)) by A2,LATTICES:31
              .= (x "/\" (y + x)) "/\" (y + y`) by LATTICES:def 7
              .= x "/\" (y + y`) by LATTICES:def 9
              .= x "/\" Top L by Th61
              .= x by A3;
    end;
    hence thesis by Def6;
  end;
end;

definition
  cluster Huntington -> Boolean (de_Morgan preOrthoLattice);
  coherence
  proof
    let L be de_Morgan preOrthoLattice;
    assume A1: L is Huntington;
    then reconsider L' = L as Huntington preOrthoLattice;
    thus L is bounded
    proof
A2:    L' is upper-bounded;
        L is lower-bounded
      proof
        set c' = Bot L';
        reconsider c = c' as Element of L;
        take c;
        let a be Element of L;
        reconsider a' = a as Element of L';
        thus c "/\" a = c' *' a' by Lm1 .= c by Def9;
        thus a "/\" c = c' *' a' by Lm1 .= c by Def9;
      end;
      hence thesis by A2,LATTICES:def 15;
    end;
    thus L is complemented
    proof
      let b be Element of L;
      take a = b`;
      A3: L' is join-idempotent;
      hence a + b = Top L by Def8;
      thus b + a = Top L by A3,Def8;
      thus a "/\" b = a *' b by Lm1
                 .= (a` + b`)` by Def4
                 .= Bot L' by Th9
                 .= Bottom L by Th63;
      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 Lm1;
      thus a "/\" (b "\/" c) = a *' (b + c) by Lm1
                        .= (a "/\" b) "\/" (a "/\" c) by A1,A4,Th31;
    end;
  end;
end;

definition
  cluster Robbins de_Morgan -> Boolean preOrthoLattice;
  coherence
  proof
    let L be preOrthoLattice;
    assume L is Robbins de_Morgan;
    then reconsider L' = L as Robbins de_Morgan preOrthoLattice;
    thus L is bounded
    proof
        L' is upper-bounded;
      hence thesis;
    end;
      now let b be Element of L';
      take a = b`;
      thus a + b = Top L' by Def8;
      thus a "/\" b = a *' b by Lm1
                 .= (a` + b`)` by Def4
                 .= Bot L' by Th9
                 .= Bottom L' by Th63;
    end;
    hence L is complemented;
      now let a, b, c be Element of L';
A1:    a "/\" b = a *' b & a "/\" c = a *' c by Lm1;
      thus a "/\" (b "\/" c) = a *' (b + c) by Lm1
                        .= (a "/\" b) "\/" (a "/\" c) by A1,Th31;
    end;
    hence L is distributive;
  end;

  cluster Boolean -> Robbins (well-complemented preOrthoLattice);
  coherence
  proof
    let L be well-complemented preOrthoLattice;
    assume L is Boolean;
    then reconsider L' = L as Boolean well-complemented preOrthoLattice;
      now let x, y be Element of L';
      thus ((x + y)` + (x + y`)`)` = (x + y) "/\" (x + y`) by Th34
             .= ((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 Th34
             .= 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 L')` by Th61
             .= x + Bottom L' by Th62
             .= x by LATTICES:39;
    end;
    hence thesis by Def5;
  end;
end;


Back to top