:: On the Two Short Axiomatizations of Ortholattices
::  by Wioletta Truszkowska and Adam Grabowski
::
:: Received June 28, 2003
:: Copyright (c) 2003-2021 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;


begin :: One Axiom for Boolean Algebra

definition
  let L be non empty ComplLLattStr;
  attr L is satisfying_DN_1 means
:: ROBBINS2:def 1

  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;
  cluster TrivOrtLat -> satisfying_DN_1;
end;

registration
  cluster join-commutative join-associative satisfying_DN_1 for non empty
    ComplLLattStr;
end;

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

theorem :: ROBBINS2:1
  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;

theorem :: ROBBINS2:2
  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;

theorem :: ROBBINS2:3
  for L being satisfying_DN_1 non empty ComplLLattStr, x being
  Element of L holds ((x + x`)` + x)` = x`;

theorem :: ROBBINS2:4
  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;

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

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

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

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

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

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

theorem :: ROBBINS2:11
  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)`;

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

theorem :: ROBBINS2:13
  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;

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

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

theorem :: ROBBINS2:16
  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)`;

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

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

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

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

theorem :: ROBBINS2:21
  for L being satisfying_DN_1 non empty ComplLLattStr, x being
  Element of L holds (x + x)` = x`;

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

theorem :: ROBBINS2:23
  for L being satisfying_DN_1 non empty ComplLLattStr, x being
  Element of L holds x`` = x;

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

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

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

theorem :: ROBBINS2:27
  for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
  Element of L holds x + y = y + x;

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

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

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

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

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

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

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

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

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

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

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

theorem :: ROBBINS2:38
  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;

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

theorem :: ROBBINS2:40
  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;

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

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

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

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

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

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

theorem :: ROBBINS2:47
  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)``;

theorem :: ROBBINS2:48
  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;

theorem :: ROBBINS2:49
  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);

theorem :: ROBBINS2:50
  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);

theorem :: ROBBINS2:51
  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);

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

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

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

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

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

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

registration
  cluster satisfying_DN_1 -> join-associative for non empty ComplLLattStr;
  cluster satisfying_DN_1 -> Robbins for non empty ComplLLattStr;
end;

theorem :: ROBBINS2:58
  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
;

theorem :: ROBBINS2:59
  for L being join-commutative join-associative non empty ComplLLattStr
   st L is Robbins holds L is satisfying_DN_1;

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

registration
  cluster satisfying_DN_1 de_Morgan for preOrthoLattice;
end;

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

begin :: Meredith Two Axioms for Boolean Algebras

definition
  let L be non empty ComplLLattStr;
  attr L is satisfying_MD_1 means
:: ROBBINS2:def 2

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

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

registration
  cluster satisfying_MD_1 satisfying_MD_2 -> join-commutative join-associative
    Huntington for non empty ComplLLattStr;
  cluster join-commutative join-associative Huntington -> satisfying_MD_1
    satisfying_MD_2 for non empty ComplLLattStr;
end;

registration
  cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan
    for preOrthoLattice;
end;

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