:: On the Two Short Axiomatizations of Ortholattices
::  by Wioletta Truszkowska and Adam Grabowski
::
:: Received June 28, 2003
:: Copyright (c) 2003-2016 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, ROBBINS1, SUBSET_1, ARYTM_3, LATTICES, ROBBINS2;
 notations STRUCT_0, LATTICES, ROBBINS1;
 constructors ROBBINS1;
 registrations LATTICES, ROBBINS1, STRUCT_0;
 theorems ROBBINS1, LATTICES, STRUCT_0;

begin :: One Axiom for Boolean Algebra

definition
  let L be non empty ComplLLattStr;
  attr L is satisfying_DN_1 means
  :Def1:
  for x, y, z, u being Element of L
  holds (((x + y)` + z)` + (x + (z` + (z + u)`)`)`)` = z;
end;

registration
  cluster TrivComplLat -> satisfying_DN_1;
  coherence
  by STRUCT_0:def 10;
  cluster TrivOrtLat -> satisfying_DN_1;
  coherence
  by STRUCT_0:def 10;
end;

registration
  cluster join-commutative join-associative satisfying_DN_1 for non empty
    ComplLLattStr;
  existence
  proof
    take TrivComplLat;
    thus thesis;
  end;
end;

reserve L for satisfying_DN_1 non empty ComplLLattStr;
reserve x, y, z for Element of L;

theorem Th1:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u,
v being Element of L holds ((x + y)` + (((z + u)` + x)` + (y` + (y + v)`)`)`)`
  = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z, u, v be Element of L;
  set X = ((z + u)` + x)`, Y = (z + (x` + (x + u)`)`)`;
  set Z = y, U = v;
  (((X + Y)` + Z)` + (X + (Z` + (Z + U)`)`)`)` = Z by Def1;
  hence thesis by Def1;
end;

theorem Th2:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u
  being Element of L holds ((x + y)` + ((z + x)` + (y` + (y + u)`)`)`)` = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z, u be Element of L;
  set v = the Element of L;
  ((x + z)` + (((y + u)` + x)` + (z` + (z + v)`)`)`)` = z by Th1;
  hence thesis by Th1;
end;

theorem Th3:
  for L being satisfying_DN_1 non empty ComplLLattStr, x being
  Element of L holds ((x + x`)` + x)` = x`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x be Element of L;
  set y = the Element of L;
  set V = (x + y)`;
  ((x + x`)` + (((x`` + y)` + x)` + (x`` + (x` + V)`)`)`)` = x` by Th1;
  hence thesis by Def1;
end;

theorem Th4:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u
being Element of L holds ((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + u)`)`
  )`)` = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z, u be Element of L;
  ((y + y`)` + y)` = y` by Th3;
  hence thesis by Th2;
end;

theorem Th5:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds ((x + y)` + ((z + x)` + y)`)` = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set u = the Element of L;
  set U = (y` + (y + u)`)`;
  ((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + U)`)`)`)` = y by Th4;
  hence thesis by Def1;
end;

theorem Th6:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds ((x + y)` + (x` + y)`)` = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set Z = (x + x`)`;
  ((x + y)` + ((Z + x)` + y)`)` = y by Th5;
  hence thesis by Th3;
end;

theorem Th7:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (((x + y)` + x)` + (x + y)`)` = x
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set X = (x + y)`;
  ((X + x)` + ((x + X)` + (((x + x`)` + x)` + (x + y)`)`)`)` = x by Th4;
  hence thesis by Th5;
end;

theorem Th8:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (x + ((x + y)` + x)`)` = (x + y)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set X = (x + y)`, Y = x;
  (((X + Y)` + X)` + (X + Y)`)` = X by Th7;
  hence thesis by Th7;
end;

theorem Th9:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds (((x + y)` + z)` + (x + z)`)` = z
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set X = (x + y)`, Y = z, Z = ((x + y)` + x)`;
  ((X + Y)` + ((Z + X)` + Y)`)` = Y by Th5;
  hence thesis by Th7;
end;

theorem Th10:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds (x + ((y + z)` + (y + x)`)`)` = (y + x)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set Z = (y + x)`, X = (y + z)`, Y = x;
  (((X + Y)` + Z)` + (X + Z)`)` = Z by Th9;
  hence thesis by Th9;
end;

theorem Th11:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds ((((x + y)` + z)` + (x` + y)`)` + y)` = (x` + y)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set X = (x + y)`, Z = (x` + y)`, Y = z;
  (((X + Y)` + Z)` + (X + Z)`)` = Z by Th9;
  hence thesis by Th6;
end;

theorem Th12:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds (x + ((y + z)` + (z + x)`)`)` = (z + x)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set Y = z, Z = ((y + x)` + (y + z)`)`;
  (x + ((Y + Z)` + (Y + x)`)`)` = (Y + x)` by Th10;
  hence thesis by Th10;
end;

theorem Th13:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u
  being Element of L holds ((x + y)` + ((z + x)` + (y` + (u + y)`)`)`)` = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z, u be Element of L;
  set U = ((u + z)` + (u + y)`)`;
  ((x + y)` + ((z + x)` + (y` + (y + U)`)`)`)` = y by Th2;
  hence thesis by Th10;
end;

theorem Th14:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (x + y)` = (y + x)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set Z = y, X = x, Y = (y + x)`;
  ((Y + Z)` + (Z + X)`)` = y by Th7;
  hence thesis by Th12;
end;

theorem Th15:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds (((x + y)` + (y + z)`)` + z)` = (y + z)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set Y = ((x + y)` + (y + z)`)`;
  (z + Y)` = (Y + z)` by Th14;
  hence thesis by Th12;
end;

theorem Th16:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds ((x + ((x + y)` + z)`)` + z)` = ((x + y)` + z)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set X = ((x + y)` + x)`, Y = (x + y)`;
  (X + Y)` = x by Th7;
  hence thesis by Th15;
end;

theorem Th17:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (((x + y)` + x)` + y)` = (y + y)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set X = (x + y)`;
  (X + ((X + x)` + y)`)` = y by Th5;
  hence thesis by Th16;
end;

theorem Th18:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (x` + (y + x)`)` = x
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set X = (y + x)`;
  (X + ((x` + y)` + (x` + X)`)`)` = x by Th13;
  hence thesis by Th10;
end;

theorem Th19:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds ((x + y)` + y`)` = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  (y` + (x + y)`)` = y by Th18;
  hence thesis by Th14;
end;

theorem Th20:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (x + (y + x`)`)` = x`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set Z = x`, X = y, Y = x;
  (((X + Y)` + Z)` + (X + Z)`)` = Z by Th9;
  hence thesis by Th19;
end;

theorem Th21:
  for L being satisfying_DN_1 non empty ComplLLattStr, x being
  Element of L holds (x + x)` = x`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x be Element of L;
  set y = the Element of L;
  set Y = (y + x)`;
  (x + (Y + x`)`)` = x` by Th20;
  hence thesis by Th19;
end;

theorem Th22:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (((x + y)` + x)` + y)` = y`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  y` = (y + y)` by Th21
    .= (((x + y)` + x)` + y)` by Th17;
  hence thesis;
end;

theorem Th23:
  for L being satisfying_DN_1 non empty ComplLLattStr, x being
  Element of L holds x`` = x
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x be Element of L;
  x`` = (((x + x`)` + x)` + x`)` by Th22
    .= x by Th19;
  hence thesis;
end;

theorem Th24:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds ((x + y)` + x)`+ y = y``
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  (((x + y)` + x)` + y)`` = y`` by Th22;
  hence thesis by Th23;
end;

theorem Th25:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (x + y)`` = y + x
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  (x + y)`` = (y + x)`` by Th14
    .= y + x by Th23;
  hence thesis;
end;

theorem Th26:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds x + ((y + z)` + (y + x)`)` = (y + x )``
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  (x + ((y + z)` + (y + x)`)`)`` = (y + x)`` by Th10;
  hence thesis by Th23;
end;

theorem Th27:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds x + y = y + x
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  x + y = (x + y)`` by Th23
    .= y + x by Th25;
  hence thesis;
end;

Lm1: for L being satisfying_DN_1 non empty ComplLLattStr holds L is
join-commutative
proof
  let L;
  for x, y holds x + y = y + x by Th27;
  hence thesis by LATTICES:def 4;
end;

registration
  cluster satisfying_DN_1 -> join-commutative for non empty ComplLLattStr;
  coherence by Lm1;
end;

theorem Th28:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds ((x + y)` + x)` + y = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  ((x + y)` + x)` + y = y`` by Th24;
  hence thesis by Th23;
end;

theorem
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds ((x + y)` + y)`+ x = x by Th28;

theorem
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds x + ((y + x)` + y)` = x by Th28;

theorem Th31:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (x + y`)` + (y` + y)` = (x + y`)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set X = (x + y`)`;
  X + ((y + X)` + y)` = X by Th28;
  hence thesis by Th20;
end;

theorem Th32:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (x + y)` + (y + y`)` = (x + y)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set X = (x + y)`, Y = y`;
  X + ((Y + X)` + Y)` = X by Th28;
  hence thesis by Th18;
end;

theorem
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (x + y)` + (y` + y)` = (x + y)` by Th32;

theorem Th34:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds ((x + y`)`` + y)` = (y` + y)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set Y = y`, Z = y;
  (((x + Y)` + (Y + Z)`)` + Z)` = (Y + Z)` by Th15;
  hence thesis by Th31;
end;

theorem Th35:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds ((x + y`) + y)` = (y` + y)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  ((x + y`)`` + y)` = (y` + y)` by Th34;
  hence thesis by Th23;
end;

theorem Th36:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds ((((x + y`) + z)` + y)` + (y` + y)`)` = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  ((x + y`) + y)` = (y` + y)` by Th35;
  hence thesis by Th9;
end;

theorem Th37:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds x + ((y + z)` + (y + x)`)` = y + x
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  x + ((y + z)` + (y + x)`)` = (y + x )`` by Th26;
  hence thesis by Th23;
end;

theorem Th38:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds x + (y + ((z + y)` + x)`)` = (z + y)` + x
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set Y = (z + y)`, Z = y`;
  x + ((Y + Z)` + (Y + x)`)` = Y + x by Th37;
  hence thesis by Th19;
end;

theorem
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
  Element of L holds x + ((y + x)` + (y + z)`)` = y + x by Th37;

theorem Th40:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds ((x + y)` + ((x + y)` + (x + z)`)`)` + y = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set Y = ((x + y)` + (x + z)`)`;
  ((y + Y)` + Y)`+ y = y by Th28;
  hence thesis by Th37;
end;

theorem Th41:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds (((x + y`) + z)` + y)`` = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  (((x + y`) + z)` + y)` + (y` + y)` = (((x + y`) + z)` + y)` by Th32;
  hence thesis by Th36;
end;

theorem Th42:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds x + ((y + x`) + z)` = x
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  (((y + x`) + z)` + x)`` = x by Th41;
  hence thesis by Th25;
end;

theorem Th43:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds x` + ((y + x) + z)` = x`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set X = x`;
  X + ((y + X`) + z)` = X by Th42;
  hence thesis by Th23;
end;

theorem Th44:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (x + y)` + x = x + y`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  set Z = x;
  x + (y + ((Z + y)` + x)`)` = (Z + y)` + x by Th38;
  hence thesis by Th28;
end;

theorem Th45:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds (x + (x + y`)`)` = (x + y)`
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y be Element of L;
  (x + ((x + y)` + x)`)` = (x + y)` by Th8;
  hence thesis by Th44;
end;

theorem Th46:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds ((x + y)` + (x + z))` + y = y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  ((x + y)` + ((x + y)` + (x + z)`)`)` = ((x + y)` + (x + z))` by Th45;
  hence thesis by Th40;
end;

theorem Th47:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = (x` + y)``
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  ((((x + y)` + z)` + (x` + y)`)` + y)`` = (x` + y)`` by Th11;
  hence thesis by Th23;
end;

theorem Th48:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = x` + y
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  (((x + y)` + z)` + (x` + y)`)` + y = (x` + y)`` by Th47;
  hence thesis by Th23;
end;

theorem Th49:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)``+
  (y + z)
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set X = (y + x)`, Y = (y + z), Z = x;
  (((X + Y)` + Z)` + (X` + Y)`)` + Y = X` + Y by Th48;
  hence thesis by Th46;
end;

theorem Th50:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + (
  y + z)
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  (x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)`` + (y + z) by Th49;
  hence thesis by Th23;
end;

theorem Th51:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x) + (y
  + z)
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + (y + z) by Th50;
  hence thesis by Th23;
end;

theorem Th52:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds x`` + (y + z) = (y + x) + (y + z)
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  x` + ((y + x) + (y + z))` = x` by Th43;
  hence thesis by Th51;
end;

theorem Th53:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds (x + y) + (x + z) = y + (x + z)
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  set Y = x, X = y;
  X`` + (Y + z) = (Y + X) + (Y + z) by Th52;
  hence thesis by Th23;
end;

theorem
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
  Element of L holds (x + y) + (x + z) = z + (x + y) by Th53;

theorem Th55:
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
  being Element of L holds x + (y + z) = z + (y + x)
proof
  let L be satisfying_DN_1 non empty ComplLLattStr;
  let x, y, z be Element of L;
  (y + x) + (y + z) = z + (y + x) by Th53;
  hence thesis by Th53;
end;

theorem
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
  Element of L holds x + (y + z) = y + (z + x) by Th55;

theorem
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
  Element of L holds (x + y) + z = x + (y + z) by Th55;

Lm2: for L being satisfying_DN_1 non empty ComplLLattStr holds L is
join-associative
proof
  let L;
  for x, y, z holds (x + y) + z = x + (y + z) by Th55;
  hence thesis by LATTICES:def 5;
end;

Lm3: L is Robbins
proof
  for x, y holds ((x + y)` + (x + y`)`)` = x by Th6;
  hence thesis by ROBBINS1:def 5;
end;

registration
  cluster satisfying_DN_1 -> join-associative for non empty ComplLLattStr;
  coherence by Lm2;
  cluster satisfying_DN_1 -> Robbins for non empty ComplLLattStr;
  coherence by Lm3;
end;

theorem Th58:
  for L being non empty ComplLLattStr, x, z being Element of L st L
  is join-commutative join-associative Huntington holds (z + x) *' (z + x`) = z
proof
  let L be non empty ComplLLattStr;
  let x, z be Element of L;
  assume L is join-commutative join-associative Huntington;
  then reconsider
  L9 = L as join-commutative join-associative Huntington non empty
  ComplLLattStr;
  reconsider z9 = z, x9 = x as Element of L9;
  (z9 + x9) *' (z9 + x9`) = z9 + (x9 *' x9`) by ROBBINS1:31
    .= z9 + Bot L9 by ROBBINS1:15
    .= z9 by ROBBINS1:13;
  hence thesis;
end;

theorem Th59:
  for L being join-commutative join-associative non empty ComplLLattStr
   st L is Robbins holds L is satisfying_DN_1
proof
  let L be join-commutative join-associative non empty ComplLLattStr;
  assume L is Robbins;
  then reconsider
  L9 = L as join-commutative join-associative Robbins non empty
  ComplLLattStr;
  let x, y, z, u be Element of L;
A1: L9 is Huntington;
  then
A2: (z + x) *' (z + x`) = z by Th58;
A3: ((x + y)` + z) *' z = (z + (x + y)`) *' z
    .= z *' (z + (x + y)`)
    .= z by A1,ROBBINS1:21;
A4: (((x + y)` + z) *' x) + z = z + (((x + y)` + z) *' x)
    .= (z + ((x + y)` + z)) *' (z + x) by A1,ROBBINS1:31
    .= (((x + y)` + z) + z) *' (z + x)
    .= ((x + y)` + (z + z)) *' (z + x) by LATTICES:def 5
    .= ((x + y)` + z) *' (z + x) by A1,ROBBINS1:12
    .= ((x` *' y`)`` + z) *' (z + x) by A1,ROBBINS1:17
    .= ((x` *' y`) + z) *' (z + x) by A1,ROBBINS1:3
    .= (z + (x` *' y`)) *' (z + x)
    .= ((z + x`) *' (z + y`)) *' (z + x) by A1,ROBBINS1:31
    .= (z + x) *' ((z + x`) *' (z + y`))
    .= (z + x) *' ((x` + z) *' (z + y`))
    .= (z + x) *' ((x` + z) *' (y` + z))
    .= (z + x) *' (x` + z) *' (y` + z) by A1,ROBBINS1:16
    .= (z + x) *' (z + x`) *' (y` + z)
    .= z *' (z + y`) by A2
    .= z by A1,ROBBINS1:21;
  (((x + y)` + z)` + (x + (z` + (z + u)`)`)`)` = (((x + y)` + z)`` *' (x +
  (z` + (z + u)`)`)``)`` by A1,ROBBINS1:17
    .= ((x + y)` + z)`` *' (x + (z` + (z + u)`)`)`` by A1,ROBBINS1:3
    .= ((x + y)` + z)`` *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:3
    .= ((x + y)` + z) *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:3
    .= ((x + y)`` *' z`)` *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:17
    .= ((x + y) *' z`)` *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:3
    .= ((x + y) *' z`)` *' (x + (z`` *' (z + u)``)``) by A1,ROBBINS1:17
    .= ((x + y) *' z`)` *' (x + (z *' (z + u)``)``) by A1,ROBBINS1:3
    .= ((x + y) *' z`)` *' (x + (z *' (z + u)``)) by A1,ROBBINS1:3
    .= ((x + y) *' z`)` *' (x + (z *' (z + u))) by A1,ROBBINS1:3
    .= ((x + y) *' z`)` *' (x + z) by A1,ROBBINS1:21
    .= (((x + y) *' z`)` *' x) + (((x + y) *' z`)` *' z) by A1,ROBBINS1:30
    .= (((x + y)`` *' z`)` *' x) + (((x + y) *' z`)` *' z) by A1,ROBBINS1:3
    .= (((x + y)` + z) *' x) + (((x + y) *' z`)` *' z) by A1,ROBBINS1:17
    .= (((x + y)` + z) *' x) + (((x + y)`` *' z`)` *' z) by A1,ROBBINS1:3
    .= z by A1,A3,A4,ROBBINS1:17;
  hence thesis;
end;

registration
  cluster join-commutative join-associative Robbins -> satisfying_DN_1 for non
    empty ComplLLattStr;
  coherence by Th59;
end;

registration
  cluster satisfying_DN_1 de_Morgan for preOrthoLattice;
  existence
  proof
    take TrivOrtLat;
    thus thesis;
  end;
end;

registration
  cluster satisfying_DN_1 de_Morgan -> Boolean for preOrthoLattice;
  coherence;
  cluster Boolean -> satisfying_DN_1 for well-complemented preOrthoLattice;
  coherence;
end;

begin :: Meredith Two Axioms for Boolean Algebras

definition
  let L be non empty ComplLLattStr;
  attr L is satisfying_MD_1 means

  for x, y being Element of L holds (x` + y)` + x = x;
  attr L is satisfying_MD_2 means

  for x, y, z being Element of L holds (x` + y)` + (z + y) = y + (z + x);
end;

Lm4: now
  let L be non empty ComplLLattStr;
  assume
A1: L is satisfying_MD_1 satisfying_MD_2;
A2: for x, y being Element of L holds x` + (x` + y) = x` + y
  proof
    let x, y be Element of L;
    set X = x` + y;
    X` + x = x by A1;
    hence thesis by A1;
  end;
A3: for x, y being Element of L holds (x` + y)` + y = y + x
  proof
    let x, y be Element of L;
    set X = x` + y;
A4: X` + (X` + y) = y + (X` + x) by A1;
    (x` + y)` + y = X` + (X` + y) by A2
      .= y + x by A1,A4;
    hence thesis;
  end;
A5: for x being Element of L holds x + x = x
  proof
    let x be Element of L;
    x + x = (x` + x)` + x by A3
      .= x by A1;
    hence thesis;
  end;
A6: for x, y being Element of L holds x + (x + y) = x + y
  proof
    let x, y be Element of L;
    x + (x + y) = (y` + x)` + (x + x) by A1
      .= (y` + x)` + x by A5
      .= x + y by A3;
    hence thesis;
  end;
A7: for x, y being Element of L holds (x + y) + y = x + y
  proof
    let x, y be Element of L;
    set Y = x + y;
    (x + y) + y = (y` + (x + y))` + (x + y) by A3
      .= (y` + (x + y))` + (x + (x + y)) by A6
      .= Y + (x + y) by A1
      .= x + y by A5;
    hence thesis;
  end;
A8: for x, y being Element of L holds (x + y) + x = x + y
  proof
    let x, y be Element of L;
    (x + y) + x = ((y` + x)` + x) + x by A3
      .= (y` + x)` + x by A7
      .= x + y by A3;
    hence thesis;
  end;
A9: for x, y being Element of L holds x + (y + (y + x)) = y + x
  proof
    let x, y be Element of L;
    set Z = y + x;
    x + (y + (y + x)) = (Z` + x)` + (y + x) by A1
      .= y + x by A1;
    hence thesis;
  end;
A10: for x, y being Element of L holds x + (y + x) = y + x
  proof
    let x, y be Element of L;
    x + (y + x) = x + (y + (y + x)) by A6
      .= y + x by A9;
    hence thesis;
  end;
A11: for x, y being Element of L holds (x + y`)` + y = y
  proof
    let x, y be Element of L;
    (x + y`)` + y = (y` + (x + y`))` + y by A10
      .= y by A1;
    hence thesis;
  end;
A12: for x being Element of L holds x`` + x = x
  proof
    let x be Element of L;
    (x` + x`)` + x = x by A1;
    hence thesis by A5;
  end;
A13: for x being Element of L holds x + x`` = x
  proof
    let x be Element of L;
    x + x`` = (x`` + x) + x`` by A12
      .= x`` + x by A8
      .= x by A12;
    hence thesis;
  end;
A14: for x, y being Element of L holds x + (x`` + y) = x + y
  proof
    let x, y be Element of L;
    x + (x`` + y) = (y` + x)` + (x`` + x) by A1
      .= (y` + x)` + x by A12
      .= x + y by A3;
    hence thesis;
  end;
A15: for x being Element of L holds x + x```` = x
  proof
    let x be Element of L;
    x + x```` = x + (x`` + x````) by A14
      .= x + x`` by A13
      .= x by A13;
    hence thesis;
  end;
A16: for x being Element of L holds x``` = x`
  proof
    let x be Element of L;
    x``` = (x + x````)` + x``` by A11
      .= x` + x``` by A15
      .= x` by A13;
    hence thesis;
  end;
A17: for x, y, z being Element of L holds (x` + y)` + ((x` + z)` + y) = y + x
  proof
    let x, y, z be Element of L;
    (x` + y)` + ((x` + z)` + y) = y + ((x` + z)` + x) by A1
      .= y + x by A1;
    hence thesis;
  end;
A18: for x, y being Element of L holds x + y`` = x + y
  proof
    let x, y be Element of L;
    x + y = (y` + x)` + ((y` + x)` + x) by A17
      .= (y` + x)` + ((y``` + x)` + x) by A16
      .= (y``` + x)` + ((y``` + x)` + x) by A16
      .= x + y`` by A17;
    hence thesis;
  end;
A19: for x being Element of L holds x`` = x
  proof
    let x be Element of L;
    x`` = (x``` + x``)` + x`` by A1
      .= (x` + x``)` + x`` by A16
      .= (x` + x``)` + x by A18
      .= x by A1;
    hence thesis;
  end;
A20: for x, y, z being Element of L holds (x` + ((y + x)` + z)`)` + (y + ((y
  + x)` + z)`) = y + x
  proof
    let x, y, z be Element of L;
    set P = ((y + x)` + z)`;
    (x` + P)` + (y + P) = P + (y + x) by A1
      .= y + x by A1;
    hence thesis;
  end;
A21: for x, y being Element of L holds (x` + (x + y)`)` + (y` + (x + y)`) =
  y` + x
  proof
    let x, y be Element of L;
    (x` + (x + y)`)` + (y` + (x + y)`) = (x` + (x + y)`)` + (y` + ((y` +
    x)` + x)`) by A3
      .= (x` + ((y` + x)` + x)`)` + (y` + ((y` + x)` + x)`) by A3
      .= y` + x by A20;
    hence thesis;
  end;
A22: for x, y being Element of L holds x + (x` + y)` = x
  proof
    let x, y be Element of L;
    x + (x` + y)` = ((x` + y)` + x) + (x` + y)` by A1
      .= (x` + y)` + x by A8
      .= x by A1;
    hence thesis;
  end;
A23: for x, y being Element of L holds x` + (x + y)` = x`
  proof
    let x, y be Element of L;
    x` = x` + (x`` + y)` by A22
      .= x` + (x + y)` by A19;
    hence thesis;
  end;
A24: for x, y being Element of L holds x + (y + x`)` = x
  proof
    let x, y be Element of L;
    x + (y + x`)` = ((y + x`)` + x) + (y + x`)` by A11
      .= (y + x`)` + x by A8
      .= x by A11;
    hence thesis;
  end;
A25: for x, y being Element of L holds x` + (y + x)` = x`
  proof
    let x, y be Element of L;
    x` = x` + (y + x``)` by A24
      .= x` + (y + x)` by A19;
    hence thesis;
  end;
A26: for x, y being Element of L holds x + y` = y` + x
  proof
    let x, y be Element of L;
    y` + x = (x` + (x + y)`)` + (y` + (x + y)`) by A21
      .= x`` + (y` + (x + y)`) by A23
      .= x`` + y` by A25
      .= x + y` by A19;
    hence thesis;
  end;
A27: for x, y being Element of L holds x + y = y + x
  proof
    let x, y be Element of L;
    y`` = y by A19;
    hence thesis by A26;
  end;
  hence L is join-commutative by LATTICES:def 4;
A28: for x, y, z being Element of L holds ((x` + y)` + z)` + (x` + z) = z + (
  x` + y)
  proof
    let x, y, z be Element of L;
    ((x` + y)` + z)` + (x` + z) = z + (x` + (x` + y)) by A1
      .= z + (x` + y) by A2;
    hence thesis;
  end;
A29: for x, y being Element of L holds x + (y` + x) = y` + x
  proof
    let x, y be Element of L;
    x + (y` + x) = ((y` + x)` + x)` + (y` + x) by A28
      .= y` + x by A1;
    hence thesis;
  end;
A30: for x, y being Element of L holds (x + y)` + x = y` + x
  proof
    let x, y be Element of L;
    set Y = y` + x;
    y` + x = x + (y` + x) by A29
      .= (Y` + x)` + x by A3
      .= (x + y)` + x by A3;
    hence thesis;
  end;
A31: for x, y being Element of L holds (x + y)` + (y` + x)` = x` + (y` + x)`
  proof
    let x, y be Element of L;
    (x + y)` + (y` + x)` = ((y` + x)` + x)` + (y` + x)` by A3
      .= x` + (y` + x)` by A30;
    hence thesis;
  end;
  for x, y being Element of L holds (x` + y`)` + (x` + y)` = x
  proof
    let x, y be Element of L;
    (x` + y`)` + (x` + y)` = (y` + x`)` + (x` + y)` by A27
      .= (x` + y)` + (y` + x`)` by A27
      .= x`` + (y` + x`)` by A31
      .= x + (y` + x`)` by A19
      .= x by A24;
    hence thesis;
  end;
  hence L is Huntington by ROBBINS1:def 6;
A32: for x, y, z being Element of L holds (x + y) + (y + z) = (x + y) + z
  proof
    let x, y, z be Element of L;
    set Y = x + y;
    (x + y) + z = (z` + Y)` + Y by A3
      .= (z` + Y)` + (y + Y) by A10
      .= Y + (y + z) by A1;
    hence thesis;
  end;
  for x, y, z being Element of L holds (x + y) + z = x + (y + z)
  proof
    let x, y, z be Element of L;
    for x, y, z being Element of L holds (x + y) + (z + x) = y + (x + z)
    proof
      let x, y, z be Element of L;
      (x + y) + (z + x) = (z + x) + (x + y) by A27
        .= (z + x) + y by A32
        .= (x + z) + y by A27
        .= y + (x + z) by A27;
      hence thesis;
    end;
    then (y + x) + (z + y) = x + (y + z);
    then
A33: (x + y) + (z + y) = x + (y + z) by A27;
    (x + y) + z = (x + y) + (y + z) by A32
      .= x + (y + z) by A27,A33;
    hence thesis;
  end;
  hence L is join-associative by LATTICES:def 5;
end;

registration
  cluster satisfying_MD_1 satisfying_MD_2 -> join-commutative join-associative
    Huntington for non empty ComplLLattStr;
  coherence by Lm4;
  cluster join-commutative join-associative Huntington -> satisfying_MD_1
    satisfying_MD_2 for non empty ComplLLattStr;
  coherence
  proof
    let L be non empty ComplLLattStr;
    assume L is join-commutative join-associative Huntington;
    then reconsider
    L9 = L as join-commutative join-associative Huntington non
    empty ComplLLattStr;
A1: L9 is satisfying_MD_2
    proof
      let x, y, z be Element of L9;
      set Z = z + y;
A2:   Z + y` = z + (y + y`) by LATTICES:def 5
        .= z + Top L9 by ROBBINS1:def 8
        .= Top L9 by ROBBINS1:19;
      (x` + y)` + (z + y) = (x` + y``)` + (z + y) by ROBBINS1:3
        .= (x *' y`) + (z + y) by ROBBINS1:def 4
        .= (Z + x) *' (Z + y`) by ROBBINS1:31
        .= Z + x by A2,ROBBINS1:14
        .= y + (z + x) by LATTICES:def 5;
      hence thesis;
    end;
    L9 is satisfying_MD_1
    proof
      let x, y be Element of L9;
      (x` + y)` + x = (x` + y``)` + x by ROBBINS1:3
        .= (x *' y`) + x by ROBBINS1:def 4
        .= x by ROBBINS1:20;
      hence thesis;
    end;
    hence thesis by A1;
  end;
end;

registration
  cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan
    for preOrthoLattice;
  existence
  proof
    take TrivOrtLat;
    thus thesis;
  end;
end;

registration
  cluster satisfying_MD_1 satisfying_MD_2 de_Morgan -> Boolean for
preOrthoLattice;
  coherence;
  cluster Boolean -> satisfying_MD_1 satisfying_MD_2 for well-complemented
    preOrthoLattice;
  coherence;
end;