SHEFFER2

:: Short {S}heffer Stroke-Based Single Axiom for {B}oolean Algebras
::  by Aneta {\L}ukaszuk and Adam Grabowski
::
:: Received May 31, 2004
:: Copyright (c) 2004-2026 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, SHEFFER1, SUBSET_1, RELAT_1, ZFMISC_1, LATTICES,
      ROBBINS1, EQREL_1, SHEFFER2;
 notations STRUCT_0, LATTICES, ROBBINS1, SHEFFER1;
 constructors SHEFFER1;
 registrations LATTICES, SHEFFER1, STRUCT_0;
 theorems ROBBINS1, SHEFFER1, STRUCT_0;

begin :: First Implication

definition
  let L be non empty ShefferStr;
  attr L is satisfying_Sh_1 means
  :Def1:
  for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | x)) = y;
end;

registration
  cluster trivial -> satisfying_Sh_1 for non empty ShefferStr;
  coherence
  by STRUCT_0:def 10;
end;

registration
  cluster satisfying_Sh_1 satisfying_Sheffer_1 satisfying_Sheffer_2
    satisfying_Sheffer_3 for non empty ShefferStr;
  existence
  proof
    take TrivShefferOrthoLattStr;
    thus thesis;
  end;
end;

reserve L for satisfying_Sh_1 non empty ShefferStr;

theorem Th1:
  for x, y, z, u being Element of L holds ((x | (y | z)) | (x | (x
| (y | z)))) | ((z | ((x | z) | z)) | (u | (x | (y | z)))) = z | ((x | z) | z)
proof
  let x, y, z, u be Element of L;
  set Y = z | ((x | z) | z);
  set X = x | (y | z);
  (X | ((Y | X) | X)) | (Y | (u | X)) = Y by Def1;
  hence thesis by Def1;
end;

theorem Th2:
  for x, y, z being Element of L holds ((x | y) | (((y | ((z | y) |
  y)) | (x | y)) | (x | y))) | z = y | ((z | y) | y)
proof
  let x, y, z be Element of L;
  set X = x | y;
  set Y = y | ((z | y) | y);
  (X | ((Y | X) | X)) | (Y | (z | X)) = Y by Def1;
  hence thesis by Def1;
end;

theorem Th3:
  for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (
  z | ((x | z) | z))) = y
proof
  let x, y, z be Element of L;
  set X = (x | z);
  set Y = (z | ((x | z) | z));
  (X | ((Y | X) | X)) | x = Y by Th2;
  hence thesis by Def1;
end;

theorem Th4:
  for x, y being Element of L holds x | ((x | ((x | x) | x)) | (y |
  (x | ((x | x) | x)))) = x | ((x |x) | x)
proof
  let x be Element of L;
  (x | ((x | x) | x)) | (x | (x | ((x | x) | x))) = x by Th3;
  hence thesis by Th1;
end;

theorem Th5:
  for x being Element of L holds x | ((x | x) | x) = x | x
proof
  let x be Element of L;
  (x | ((x | x) | x)) | (x | (x | ((x | x) | x))) = x by Th3;
  hence thesis by Th4;
end;

theorem Th6:
  for x being Element of L holds (x | ((x | x) | x )) | (x | x) = x
proof
  let x be Element of L;
  x | ((x | x) | x) = x | x by Th5;
  hence thesis by Def1;
end;

theorem Th7:
  for x, y being Element of L holds (x | x) | (x | (y | x)) = x
proof
  let x, y be Element of L;
  x | ((x | x) | x) = x | x by Th5;
  hence thesis by Def1;
end;

theorem Th8:
  for x, y being Element of L holds (x | (((y | y) | x) | x)) | y = y | y
proof
  let x, y be Element of L;
  set Y = y | y;
  set X = x | y;
  Y | (y | (X | y)) = y by Th7;
  hence thesis by Th3;
end;

theorem Th9:
  for x, y being Element of L holds ((x | y) | (((x | y) | (x | y))
  | (x | y))) | ((x | y) | (x | y)) = y | ((((x | y) | (x | y )) | y) | y)
proof
  let x, y be Element of L;
  y | ((((x | y) | (x | y)) | y) | y) | (x | y) = (x | y) | (x | y) by Th8;
  hence thesis by Th2;
end;

theorem Th10:
  for x, y being Element of L holds x | ((((y | x) | (y | x)) | x
  ) | x) = y | x
proof
  let x, y be Element of L;
  ((y | x) | (((y | x) | (y | x)) | (y | x))) |((y | x) | (y | x)) = y | x
  by Th6;
  hence thesis by Th9;
end;

theorem Th11:
  for x, y being Element of L holds (x | x) | (y | x) = x
proof
  let x, y be Element of L;
  set Y = y | x;
  x | (((Y | Y) | x) | x) = Y by Th10;
  hence thesis by Th7;
end;

theorem Th12:
  for x, y being Element of L holds x | (y | (x | x)) = x | x
proof
  let x, y be Element of L;
  set Y = (x | x);
  Y | (x | x) = x by Th11;
  hence thesis by Th11;
end;

theorem Th13:
  for x, y being Element of L holds ((x | y) | (x | y)) | y = x | y
proof
  let x, y be Element of L;
  (y | y) | (x | y) = y by Th11;
  hence thesis by Th11;
end;

theorem Th14:
  for x, y being Element of L holds x | ((y | x) | x) = y | x
proof
  let x, y be Element of L;
  ((y | x) | (y | x)) | x = y | x by Th13;
  hence thesis by Th10;
end;

theorem Th15:
  for x, y, z being Element of L holds (x | y) | (x | (z | y)) = x
proof
  let x, y, z be Element of L;
  y | ((x | y) | y) = x | y by Th14;
  hence thesis by Def1;
end;

theorem Th16:
  for x, y, z being Element of L holds (x | (y | z)) | (x | z) = x
proof
  let x, y, z be Element of L;
  (z | z) | (y | z) = z by Th11;
  hence thesis by Th15;
end;

theorem Th17:
  for x, y, z being Element of L holds x | ((x | y) | (z | y)) = x | y
proof
  let x, y, z be Element of L;
  (x | y) | (x | (z | y)) = x by Th15;
  hence thesis by Th16;
end;

theorem Th18:
  for x, y, z being Element of L holds ((x | (y | z)) | z) | x = x | (y | z)
proof
  let x, y, z be Element of L;
  set X = y | z;
  (x | X) | (x | z) = x by Th16;
  hence thesis by Th15;
end;

theorem Th19:
  for x, y being Element of L holds x | ((y | x) | x) = x | y
proof
  let x, y be Element of L;
  (x | ((y | x) | x)) | (y | ((y | x) | x)) = y by Def1;
  hence thesis by Th17;
end;

theorem Th20:
  for x, y being Element of L holds x | y = y | x
proof
  let x, y be Element of L;
  x | ((y | x) | x) = y | x by Th14;
  hence thesis by Th19;
end;

theorem Th21:
  for x, y being Element of L holds (x | y) | (x | x) = x
proof
  let x, y be Element of L;
  set X = x | y;
  x | ((y | x) | x) = X by Th19;
  hence thesis by Th16;
end;

theorem Th22:
  for x, y, z being Element of L holds (x | y) | (y | (z | x)) = y
proof
  let x, y, z be Element of L;
  set Y = x | ((y | x) | x);
  Y = x | y by Th19;
  hence thesis by Def1;
end;

theorem Th23:
  for x, y, z being Element of L holds (x | (y | z)) | (z | x) = x
proof
  let x, y, z be Element of L;
  z | x = x | z by Th20;
  hence thesis by Th16;
end;

theorem Th24:
  for x, y, z being Element of L holds (x | y) | (y | (x | z)) = y
proof
  let x, y, z be Element of L;
  z | x = x | z by Th20;
  hence thesis by Th22;
end;

theorem Th25:
  for x, y, z being Element of L holds (x | (y | z)) | (y | x) = x
proof
  let x, y, z be Element of L;
  z | y = y | z by Th20;
  hence thesis by Th23;
end;

theorem Th26:
  for x, y, z being Element of L holds ((x | y) | (x | z)) | z = x | z
proof
  let x, y, z be Element of L;
  (x | z) | (z | (x | y)) = z by Th24;
  hence thesis by Th22;
end;

theorem Th27:
  for x, y, z being Element of L holds x | (y | (x | (y | z))) = x | (y | z)
proof
  let x, y, z be Element of L;
  set Y = y | x;
  (x | (y | z)) | Y = x by Th25;
  hence thesis by Th25;
end;

theorem Th28:
  for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (x | z)
proof
  let x, y, z be Element of L;
  set Y = y | (x | z);
  Y | (x | y) = y by Th25;
  hence thesis by Th24;
end;

theorem Th29:
  for x, y, z, u being Element of L holds (x | (y | z))| (x | (u |
  (y | x))) = (x | (y | z)) | (y | x)
proof
  let x, y, z, u be Element of L;
  set X = x | (y | z);
  set Y = y | x;
  X | Y = x by Th25;
  hence thesis by Th17;
end;

theorem Th30:
  for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (z | x)
proof
  let x, y, z be Element of L;
  z | x = x | z by Th20;
  hence thesis by Th28;
end;

theorem Th31:
  for x, y, z, u being Element of L holds (x | (y | z)) | (x | (u
  | (y | x))) = x
proof
  let x, y, z be Element of L;
  (x | (y | z)) | (y | x) = x by Th25;
  hence thesis by Th29;
end;

theorem Th32:
  for x, y being Element of L holds x | (y | (x | y)) = x | x
proof
  let x, y be Element of L;
  (x | y) | (x | ((x | y) | y)) = x by Th15;
  hence thesis by Th30;
end;

theorem Th33:
  for x, y, z being Element of L holds x | (y | z) = x | (z | y)
proof
  let x, y, z be Element of L;
  (z | (x | (z | y))) | x = x | (z | y) by Th28;
  hence thesis by Th30;
end;

theorem Th34:
  for x, y, z being Element of L holds x | (y | (x | (z | (y | x)) )) = x | x
proof
  let x, y, z be Element of L;
  (x | (y | (x | (z | (y | x))))) | (x | (z | (y | x))) = x by Th31;
  hence thesis by Th18;
end;

theorem Th35:
  for x, y, z being Element of L holds (x | (y | z)) | ((y |x) | x
  ) = (x | (y | z)) | (x | (y | z))
proof
  let x, y, z be Element of L;
  set X = x | (y | z);
  X | (y | x) = x by Th25;
  hence thesis by Th32;
end;

theorem Th36:
  for x, y being Element of L holds (x | (y | x)) | y = y | y
proof
  let x, y be Element of L;
  set X = x;
  set Y = y;
  Y | (X | (Y | X)) = (X | (Y | X)) | Y by Th20;
  hence thesis by Th32;
end;

theorem Th37:
  for x, y, z being Element of L holds (x | y) | z = z | (y | x)
proof
  let x, y, z be Element of L;
  set X = x | y;
  X | z = z | X by Th20;
  hence thesis by Th33;
end;

theorem Th38:
  for x, y, z being Element of L holds x | (y | (z | (x | y))) = x | (y | y)
proof
  let x, y, z be Element of L;
  set Y = z;
  y | (x | (y | (Y | (x | y)))) = y | y by Th34;
  hence thesis by Th27;
end;

theorem Th39:
  for x, y, z being Element of L holds ((x | y) | y) | (y | (z | x
  )) = (y | (z | x)) | (y | (z | x))
proof
  let x, y, z be Element of L;
  set X = y | (z | x);
  X | (x | y) = y by Th23;
  hence thesis by Th36;
end;

theorem Th40:
  for x, y, z, u being Element of L holds (x | y) | (z | u) = (u | z) | (y | x)
proof
  let x, y, z, u be Element of L;
  (x | y) | (z | u) = (x | y) | (u | z) by Th33;
  hence thesis by Th37;
end;

theorem Th41:
  for x, y, z being Element of L holds x | (y | ((y | x) | z)) = x | (y | y)
proof
  let x, y, z be Element of L;
  x | (y | (z | (x | y))) = x | (y | ((y | x) | z)) by Th37;
  hence thesis by Th38;
end;

theorem Th42:
  for x, y being Element of L holds x | (y | x) = x | (y | y)
proof
  let x, y be Element of L;
  set Y = x | (y | y);
  Y | (x | y) = x by Th16;
  hence thesis by Th38;
end;

theorem Th43:
  for x, y being Element of L holds (x | y) | y = y | (x | x)
proof
  let x, y be Element of L;
  set X = x;
  set Y = y;
  Y | (X | Y) = (X | Y) | Y by Th20;
  hence thesis by Th42;
end;

theorem Th44:
  for x, y being Element of L holds x | (y | y) = x | (x | y)
proof
  let x, y be Element of L;
  x | (y | x) = x | (y | y) by Th42;
  hence thesis by Th33;
end;

theorem Th45:
  for x, y, z being Element of L holds (x | (y | y)) | (x | (z | y
  )) = (x | (z | y)) | (x | (z | y))
proof
  let x, y, z be Element of L;
  set Y = y;
  set X = x;
  (Y | X) | X = X | (Y | Y) by Th43;
  hence thesis by Th39;
end;

theorem Th46:
  for x, y, z being Element of L holds (x | (y | z)) | (x | (y | y
  )) = (x | (y | z)) | (x | (y | z))
proof
  let x, y, z be Element of L;
  (x | (y | z)) | ((y |x) | x) = (x | (y | z)) | (x | (y | y)) by Th43;
  hence thesis by Th35;
end;

theorem Th47:
  for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x
  | y)))) = x | ((y | y) | (y | y))
proof
  let x, y, z be Element of L;
  x | (y | y) = x | (x | y) by Th44;
  hence thesis by Th38;
end;

theorem Th48:
  for x, y, z being Element of L holds ((x | (y | z)) | (x | (y |
  z))) | (y | y) = x | (y | y)
proof
  let x, y, z be Element of L;
  set Z = (y | y);
  set Y = (y | z);
  (x | Y) | (x | Y) = (x | Y) | (x | Z) by Th46;
  hence thesis by Th26;
end;

theorem Th49:
  for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x
  | y)))) = x | y
proof
  let x, y, z be Element of L;
  (y | y) | (y | y) = y by Th21;
  hence thesis by Th47;
end;

theorem Th50:
  for x, y, z being Element of L holds (((x | y) | (x | y)) | ((z
  | ((x | y) | z)) | (x | y))) | (x | x) = (z | ((x | y) | z)) | (x | x)
proof
  let x, y, z be Element of L;
  set Y = z;
  set X = x | y;
  (Y | (X | Y)) | X = X | X by Th36;
  hence thesis by Th48;
end;

theorem Th51:
  for x, y, z being Element of L holds (x | ((y | z) | x)) | (y |
  y) = (y | z) | (y | y)
proof
  let x, y, z be Element of L;
  set Y = y | z;
  set X = x | ((y | z) | x);
  (Y | Y) | (X | Y) = Y by Th11;
  hence thesis by Th50;
end;

theorem Th52:
  for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = y
proof
  let x, y, z be Element of L;
  (y | z) | (y | y) = y by Th21;
  hence thesis by Th51;
end;

theorem Th53:
  for x, y, z being Element of L holds x | ((y | ((x | z) | y)) |
  x) = y | ((x | z) | y)
proof
  let x, y, z be Element of L;
  (y | ((x | z) | y)) | (x | x) = x by Th52;
  hence thesis by Th16;
end;

theorem Th54:
  for x, y, z being Element of L holds x | ((y | (y | (z | x))) |
  x) = y | ((x | (y | (x | z))) | y)
proof
  let x, y, z be Element of L;
  set Z = y | (x | z);
  (x | Z) | y = y | (z | x) by Th30;
  hence thesis by Th53;
end;

theorem Th55:
  for x, y, z being Element of L holds x | ((y | (y | (z | x))) |
  x) = y | (y | (z | x))
proof
  let x, y, z be Element of L;
  y | (z | x) = (x | (y | (x | z))) | y by Th30;
  hence thesis by Th54;
end;

theorem Th56:
  for x, y, z, u being Element of L holds x | (y | (z | (z | (u |
  (y | x))))) = x | (y | y)
proof
  let x, y, z, u be Element of L;
  (y | x) | (z | (z | (u | (y | x))) | (y | x)) = z | (z | (u | (y | x)))
  by Th55;
  hence thesis by Th41;
end;

theorem Th57:
  for x, y, z being Element of L holds x | (y | (y | (z | (x | y))
  )) = x | (y | (x | x))
proof
  let x, y, z be Element of L;
  y | (x | (y | (y | (z | (x | y))))) = y | (x | x) by Th56;
  hence thesis by Th27;
end;

theorem Th58:
  for x, y, z being Element of L holds x | (y | (y | (z | (x | y)) )) = x | x
proof
  let x, y, z be Element of L;
  x | (y | (x | x)) = x | x by Th12;
  hence thesis by Th57;
end;

theorem Th59:
  for x, y being Element of L holds x | (y | (y | y)) = x | x
proof
  let x, y be Element of L;
  set Y = y | (x | y);
  Y | (x | y) = y by Th25;
  hence thesis by Th58;
end;

theorem Th60:
  for x, y, z being Element of L holds x | (((y | (z | x)) | (y |
  (z | x))) | (z | z)) = x | (y | (z | x))
proof
  let x, y, z be Element of L;
  set Y = y | (z | x);
  z | (x | (x | Y)) = z | z by Th58;
  hence thesis by Th49;
end;

theorem Th61:
  for x, y, z being Element of L holds x | (y | (z | z)) = x | (y | (z | x))
proof
  let x, y, z be Element of L;
  (y | (z | x)) | (y | (z | x)) | (z | z) = y | (z | z) by Th48;
  hence thesis by Th60;
end;

theorem Th62:
  for x, y, z being Element of L holds x | (y | ((z | z) | x)) = x | (y | z)
proof
  let x, y, z be Element of L;
  set X = z | z;
  X | (z | z) = z by Th21;
  hence thesis by Th61;
end;

theorem Th63:
  for x, y, z being Element of L holds (x | (y | y)) | (x | (z | (
  (y | y) | x))) = (x | (z | y)) | (x | (z | y))
proof
  let x, y, z be Element of L;
  (x | (z | ((y | y) | x))) = (x | (z | y)) by Th62;
  hence thesis by Th45;
end;

theorem Th64:
  for x, y, z being Element of L holds (x | (y | y)) | (x | (z | (
  x | (y | y)))) = (x | (z | y)) | (x | (z |y))
proof
  let x, y, z be Element of L;
  x | (y | y) = (y | y) | x by Th37;
  hence thesis by Th63;
end;

theorem Th65:
  for x, y, z being Element of L holds (x | (y | y)) | (x | (z | z
  )) = (x | (z | y)) | (x | (z | y))
proof
  let x, y, z be Element of L;
  set X = x | (y | y);
  (x | (y | y)) | (x | (z | z)) = (x | (y | y)) | (x | (z | X)) by Th61;
  hence thesis by Th64;
end;

theorem Th66:
  for x, y, z being Element of L holds ((x | x) | y) | ((z | z) |
  y) = (y | (x | z)) | (y | (x | z))
proof
  let x, y, z be Element of L;
  (y | (z | z)) | (y | (x | x)) = ((x | x) | y) | ((z | z) | y) by Th40;
  hence thesis by Th65;
end;

theorem Th67:
  for L being non empty ShefferStr st L is satisfying_Sh_1 holds L
  is satisfying_Sheffer_1
proof
  let L be non empty ShefferStr;
  assume L is satisfying_Sh_1;
  then for x being Element of L holds (x | x) | (x | x) = x by Th21;
  hence thesis by SHEFFER1:def 13;
end;

theorem Th68:
  for L being non empty ShefferStr st L is satisfying_Sh_1 holds L
  is satisfying_Sheffer_2
proof
  let L be non empty ShefferStr;
  assume L is satisfying_Sh_1;
  then for x, y being Element of L holds x | (y | (y | y)) = x | x by Th59;
  hence thesis by SHEFFER1:def 14;
end;

theorem Th69:
  for L being non empty ShefferStr st L is satisfying_Sh_1 holds L
  is satisfying_Sheffer_3
proof
  let L be non empty ShefferStr;
  assume L is satisfying_Sh_1;
  then
  for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y
  | y) | x) | ((z | z) | x) by Th66;
  hence thesis by SHEFFER1:def 15;
end;

registration
  cluster properly_defined Boolean well-complemented Lattice-like de_Morgan
satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1
    for non empty ShefferOrthoLattStr;
  existence
  proof
    take TrivShefferOrthoLattStr;
    for x, y being Element of TrivShefferOrthoLattStr holds x "/\" y = (x`
    "\/" y`)` by STRUCT_0:def 10;
    hence thesis by ROBBINS1:def 23;
  end;
end;

registration
  cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
    properly_defined -> Boolean Lattice-like for
non empty ShefferOrthoLattStr;
  coherence by SHEFFER1:37;
  cluster Boolean Lattice-like well-complemented properly_defined ->
    satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for
non empty
    ShefferOrthoLattStr;
  coherence by SHEFFER1:26,27,28;
end;

begin :: Second Implication

reserve L for satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
  non empty ShefferStr;
reserve v,q,p,w,z,y,x for Element of L;

theorem Th70:
  for x,w holds w | ((x | x) | x) = w | w
proof
  let x,w;
  (x | x) | (x | x) = x by SHEFFER1:def 13;
  hence thesis by SHEFFER1:def 14;
end;

theorem Th71:
  for p,x holds x = (x | x) | (p | (p | p))
proof
  let p,x;
  (x | x) | (x | x) = x by SHEFFER1:def 13;
  hence thesis by SHEFFER1:def 14;
end;

theorem Th72:
  for y,w holds (w | w) | (w | (y | (y | y))) = w
proof
  let y,w;
  w | w = w | (y | (y | y)) by SHEFFER1:def 14;
  hence thesis by SHEFFER1:def 13;
end;

theorem Th73:
  for q,p,y,w holds (((w | (y | (y | y))) | p) | ((q | q) | p)) =
  ((p | (w | q)) | (p | (w | q)))
proof
  let q,p,y,w;
  (w | w) = (w | (y | (y | y))) by SHEFFER1:def 14;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th74:
  for q,p,x holds (x | p) | ((q | q) | p) = ((p | ((x | x) | q)) |
  (p | ((x | x) | q)))
proof
  let q,p,x;
  (x | x) | (x | x) = x by SHEFFER1:def 13;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th75:
  for w,p,y,q holds (((w | w) | p) | ((q | (y | (y | y))) | p)) =
  ((p | (w | q)) | (p | (w | q)))
proof
  let w,p,y,q;
  q | q = q | (y | (y | y)) by SHEFFER1:def 14;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th76:
  for p,x holds x = (x | x) | ((p | p) | p)
proof
  let p,x;
  (x | x) | (x | x) = x by SHEFFER1:def 13;
  hence thesis by Th70;
end;

theorem Th77:
  for y,w holds (w | w) | (w | ((y | y) | y)) = w
proof
  let y,w;
  w | w = w | ((y | y) | y) by Th70;
  hence thesis by SHEFFER1:def 13;
end;

theorem Th78:
  for y,w holds ((w | ((y | y) | y)) | (w | w)) = w
proof
  let y,w;
  w | w = w | ((y | y) | y) by Th70;
  hence thesis by SHEFFER1:def 13;
end;

theorem Th79:
  for p,y,w holds ((w | ((y | y) | y)) | (p | (p | p))) = w
proof
  let p,y,w;
  w | w = (w | ((y | y) | y)) by Th70;
  hence thesis by Th71;
end;

theorem Th80:
  for p,x,y holds (((y | (x | x)) | (y | (x | x))) | (p | (p | p))
  ) = ((x | x) | y)
proof
  let p,x,y;
  (((x | x) | y) | ((x | x) | y)) = ((y | (x | x)) | (y | (x | x))) by
SHEFFER1:def 15;
  hence thesis by Th71;
end;

theorem Th81:
  for x,y holds y | (x | x) = (x | x) | y
proof
  now
    let p,x,y;
    (((y | (x | x)) | (y | (x | x))) | (p | (p | p))) = y | (x | x) by Th71;
    hence y | (x | x) = (x | x) | y by Th80;
  end;
  hence thesis;
end;

theorem Th82:
  for y,w holds w | y = ((y | y) | (y | y)) | w
proof
  let y,w;
  (y | y) | (y | y) = y by SHEFFER1:def 13;
  hence thesis by Th81;
end;

theorem Th83:
  for y,w holds w | y = y | w
proof
  let y,w;
  (y | y) | (y | y) = y by SHEFFER1:def 13;
  hence thesis by Th82;
end;

theorem Th84:
  for x,p holds (p | x) | (p | ((x | x) | (x | x))) = (((x | x) |
  (x | x)) | p) | (((x | x) | (x | x)) | p)
proof
  let x,p;
  (x | x) | (x | x) = x by SHEFFER1:def 13;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th85:
  for x,p holds (p | x) | (p | x) = (((x | x) | (x | x)) | p) | ((
  (x | x) | (x | x)) | p)
proof
  let x,p;
  (x | x) | (x | x) = x by SHEFFER1:def 13;
  hence thesis by Th84;
end;

theorem Th86:
  for x,p holds (p | x) | (p | x) = (x | p) | (((x | x) | (x | x)) | p)
proof
  let x,p;
  (x | x) | (x | x) = x by SHEFFER1:def 13;
  hence thesis by Th85;
end;

theorem Th87:
  for x,p holds (p | x) | (p | x) = (x | p) | (x | p)
proof
  let x,p;
  (x | x) | (x | x) = x by SHEFFER1:def 13;
  hence thesis by Th86;
end;

theorem Th88:
  for y,q,w holds ((w | q) | ((y | y) | y)) | ((w | q) | (w | q))
  = ((w | w) | (w | q)) | ((q | q) | (w | q))
proof
  let y,q,w;
  (w | q) | (w | q) = (w | q) | ((y | y) | y) by Th70;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th89:
  for q,w holds w | q = ((w | w) | (w | q)) | ((q | q) | (w | q))
proof
  now
    let y,q,w;
    (((w | q) | ((y | y) | y)) | ((w | q) | (w | q))) = (w | q) by Th78;
    hence w | q = ((w | w) | (w | q)) | ((q | q) | (w | q)) by Th88;
  end;
  hence thesis;
end;

theorem Th90:
  for q,p holds ((p | p) | (p | ((q | q) | q))) = ((((q | q) | (q
  | q)) | p) | ((q | q) | p))
proof
  let q,p;
  p | ((q | q) | q) = p | p by Th70;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th91:
  for p,q holds p = ((((q | q) | (q | q)) | p) | ((q | q) | p))
proof
  let p,q;
  (p | p) | (p | ((q | q) | q)) = p by Th77;
  hence thesis by Th90;
end;

theorem Th92:
  for p,q holds p = (q | p) | ((q | q) | p)
proof
  let p,q;
  (q | q) | (q | q) = q by SHEFFER1:def 13;
  hence thesis by Th91;
end;

theorem Th93:
  for z,w,x holds ((((x | x) | w) | ((z | z) | w)) | ((w | (x | z)
) | (w | (x | z)))) = (((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w |
  (x | z))))
proof
  let z,w,x;
  ((w | (x | z)) | (w | (x | z))) = (((x | x) | w) | ((z | z) | w)) by
SHEFFER1:def 15;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th94:
  for z,w,x holds ((((x | x) | w) | ((z | z) | w)) | ((w | (x | z)
  ) | (w | (x | z)))) = (w | (x | z))
proof
  let z,w,x;
  (((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w | (x | z)))) = (w
  | (x | z)) by Th89;
  hence thesis by Th93;
end;

theorem Th95:
  for w,p holds ((p | p) | (p | (w | (w | w)))) = (((w | w) | p) |
  (((w | w) | (w | w)) | p))
proof
  let w,p;
  p | (w | (w | w)) = p | p by SHEFFER1:def 14;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th96:
  for p,w holds p = ((w | w) | p) | (((w | w) | (w | w)) | p)
proof
  let p,w;
  (p | p) | (p | (w | (w | w))) = p by Th72;
  hence thesis by Th95;
end;

theorem Th97:
  for p,w holds p = (((w | w) | p) | (w | p))
proof
  let p,w;
  (w | w) | (w | w) = w by SHEFFER1:def 13;
  hence thesis by Th96;
end;

theorem Th98:
  for z,q,x holds ((((x | x) | q) | ((z | z) | q)) | ((q | (x | z)
) | (q | (x | z)))) = ((((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x |
  x) | q)))
proof
  let z,q,x;
  (((x | x) | q) | ((z | z) | q)) = ((q | (x | z)) | (q | (x | z))) by
SHEFFER1:def 15;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th99:
  for q,z,x holds (q | (x | z)) = ((((z | z) | (z | z)) | ((x | x)
  | q)) | ((q | q) | ((x | x) | q)))
proof
  let q,z,x;
  ((((x | x) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z)))) = (q
  | (x | z)) by Th94;
  hence thesis by Th98;
end;

theorem Th100:
  for q,z,x holds (q | (x | z)) = ((z | ((x | x) | q)) | ((q | q)
  | ((x | x) | q)))
proof
  let q,z,x;
  (z | z) | (z | z) = z by SHEFFER1:def 13;
  hence thesis by Th99;
end;

theorem Th101:
  for w,y holds w | w = ((y | y) | y) | w
proof
  let w,y;
  w | ((y | y) | y) = w | w by Th70;
  hence thesis by Th83;
end;

theorem Th102:
  for w,p holds ((p | w) | ((w | w) | p)) = p
proof
  let w,p;
  w | p = p | w by Th83;
  hence thesis by Th92;
end;

theorem Th103:
  for y,w holds ((w | w) | ((w | w) | ((y | y) | y))) = (y | y) | y
proof
  let y,w;
  w | ((y | y) | y) = w | w by Th70;
  hence thesis by Th92;
end;

theorem Th104:
  for y,w holds (w | w) | w = (y | y) | y
proof
  let y,w;
  (w | w) | ((y | y) | y) = w by Th76;
  hence thesis by Th103;
end;

theorem Th105:
  for p,w holds (w | p) | (p | (w | w)) = p
proof
  let p,w;
  (w | w) | p = p | (w | w) by Th83;
  hence thesis by Th92;
end;

theorem Th106:
  for w,p holds (p | (w | w)) | (w | p) = p
proof
  let w,p;
  (w | w) | p = p | (w | w) by Th83;
  hence thesis by Th97;
end;

theorem Th107:
  for p,w holds (w | p) | (w | (p | p)) = w
proof
  let p,w;
  (p | p) | w = w | (p | p) by Th83;
  hence thesis by Th102;
end;

theorem Th108:
  for x,y holds (y | (((y | (x | x)) | (y | (x | x))) | (x | y))) = x | y
proof
  let x,y;
  (x | y) | (y | (x | x)) = y by Th105;
  hence thesis by Th102;
end;

theorem Th109:
  for p,w holds (w | (p | p)) | (w | p) = w
proof
  let p,w;
  p | w = w | p by Th83;
  hence thesis by Th106;
end;

theorem Th110:
  for p,w,q,y holds (((y | y) | y) | q) | ((w | w) | q) = (q | ((
(p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) |
  w))
proof
  let p,w,q,y;
  (((p | (p | p)) | (p | (p | p))) | (p | (p | p))) = (y | y) | y by Th104;
  hence thesis by Th73;
end;

theorem Th111:
  for q,w,p holds (q | q) | ((w | w) | q) = (q | (((p | (p | p))
  | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w))
proof
  let q,w,p;
  (((p | (p | p)) | (p | (p | p))) | (p | (p | p))) | q = q | q by Th101;
  hence thesis by Th73;
end;

theorem Th112:
  for w,y,p holds (w | p) | (w | (p | (y | (y | y)))) = w
proof
  let w,y,p;
  p | p = p | (y | (y | y)) by SHEFFER1:def 14;
  hence thesis by Th107;
end;

theorem Th113:
  for w,y,p holds (w | (p | (y | (y | y)))) | (w | p) = w
proof
  let w,y,p;
  p | p = p | (y | (y | y)) by SHEFFER1:def 14;
  hence thesis by Th109;
end;

theorem Th114:
  for q,p,y holds (((y | y) | y) | p) | ((q | q) | p) = (p | ((p
  | p) | q)) | (p | ((p | p) | q))
proof
  let q,p,y;
  p | p = ((y | y) | y) | p by Th101;
  hence thesis by Th74;
end;

theorem Th115:
  for q,z,x holds (((q | ((x | x) | z)) | (q | ((x | x) | z))) |
((x | q) | ((z | z) | q))) = ((((z | z) | (z | z)) | (x | q)) | ((q | q) | (x |
  q)))
proof
  let q,z,x;
  ((x | q) | ((z | z) | q)) = ((q | ((x | x) | z)) | (q | ((x | x) | z)))
  by Th74;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th116:
  for q,z,x holds (((q | ((x | x) | z)) | (q | ((x | x) | z))) |
  ((x | q) | ((z | z) | q))) = ((z | (x | q)) | ((q | q) | (x | q)))
proof
  let q,z,x;
  (z | z) | (z | z) = z by SHEFFER1:def 13;
  hence thesis by Th115;
end;

theorem Th117:
  for w,q,z holds (((w | w) | ((z | z) | q)) | ((q | ((q | q) | z
)) | (q | ((q | q) | z)))) = (((z | z) | q) | (w | q)) | (((z | z) | q) | (w |
  q))
proof
  let w,q,z;
  (q | q) | ((z | z) | q) = ((q | ((q | q) | z)) | (q | ((q | q) | z))) by Th74
;
  hence thesis by SHEFFER1:def 15;
end;

theorem Th118:
  for q,p,x holds (((p | (x | p)) | (p | (x | p))) | (q | (q | q)
  )) = (x | x) | p
proof
  let q,p,x;
  (((x | x) | p) | ((p | p) | p)) = ((p | (x | p)) | (p | (x | p))) by
SHEFFER1:def 15;
  hence thesis by Th79;
end;

theorem Th119:
  for p,x holds p | (x | p) = (x | x) | p
proof
  now
    let q,p,x;
    (((p | (x | p)) | (p | (x | p))) | (q | (q | q))) = (p | (x | p)) by Th71;
    hence p | (x | p) = (x | x) | p by Th118;
  end;
  hence thesis;
end;

theorem Th120:
  for p,y holds (y | p) | ((y | y) | p) = (p | p) | (y | p)
proof
  let p,y;
  p | (y | p) = (y | y) | p by Th119;
  hence thesis by Th119;
end;

theorem Th121:
  for x,y holds x = (x | x) | (y | x)
proof
  let x,y;
  (y | x) | ((y | y) | x) = x by Th92;
  hence thesis by Th120;
end;

theorem Th122:
  for x,y holds (y | x) | x = ((x | (y | y)) | (x | (y | y))) | ( y | x)
proof
  let x,y;
  (x | (y | y)) | (y | x) = x by Th106;
  hence thesis by Th119;
end;

theorem Th123:
  for x,z,y holds (((x | ((y | y) | z)) | (x | ((y | y) | z))) |
  ((y | x) | ((z | z) | x))) = (z | (y | x)) | x
proof
  let x,z,y;
  (x | x) | (y | x) = x by Th121;
  hence thesis by Th116;
end;

theorem Th124:
  for x,y,z holds ((x | (((z | (z | z)) | (z | (z | z))) | y)) |
  (x | (((z | (z | z)) | (z | (z | z))) | y))) = x
proof
  let x,y,z;
  (x | x) | ((y | y) | x) = x by Th121;
  hence thesis by Th111;
end;

theorem Th125:
  for x,z,y holds (x | ((y | y) | z)) | z = z | (y | x)
proof
  let x,z,y;
  (z | z) | ((y | y) | z) = z by Th121;
  hence thesis by Th100;
end;

theorem Th126:
  for x,y holds x | ((y | x) | x) = y | x
proof
  let x,y;
  ((x | (y | y)) | (x | (y | y))) | (y | x) = (y | x) | x by Th122;
  hence thesis by Th108;
end;

theorem Th127:
  for z,y,x holds y = (((x | x) | x) | y) | ((z | z) | y)
proof
  now
    let x,y,z,p;
    ((y | (((p | (p | p)) | (p | (p | p))) | z)) | (y | (((p | (p | p)) |
    (p | (p | p))) | z))) = y by Th124;
    hence y = (((x | x) | x) | y) | ((z | z) | y) by Th110;
  end;
  hence thesis;
end;

theorem Th128:
  for z,y holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y
proof
  now
    let z,y,x;
    (((x | x) | x) | y) | ((z | z) | y) = y by Th127;
    hence (y | ((y | y) | z)) | (y | ((y | y) | z)) = y by Th114;
  end;
  hence thesis;
end;

theorem Th129:
  for x,z,y holds (((y | y) | z) | (x | z)) | (((y | y) | z) | (x
  | z)) = ((x | x) | ((y | y) | z)) | z
proof
  let x,z,y;
  ((z | ((z | z) | y)) | (z | ((z | z) | y))) = z by Th128;
  hence thesis by Th117;
end;

theorem Th130:
  for x,z,y holds ((((y | y) | z) | (x | z)) | (((y | y) | z) | (
  x | z))) = z | (y | (x | x))
proof
  let x,z,y;
  (((x | x) | ((y | y) | z)) | z) = z | (y | (x | x)) by Th125;
  hence thesis by Th129;
end;

theorem Th131:
  for y,x holds ((x | y) | (x | y)) | x = x | y
proof
  let y,x;
  (x | (y | y)) | (x | y) = x by Th109;
  hence thesis by Th121;
end;

theorem Th132:
  for p,w holds (w | w) | (w | p) = w
proof
  let p,w;
  p | w = w | p by Th83;
  hence thesis by Th121;
end;

theorem Th133:
  for w,p holds (p | w) | (w | w) = w
proof
  let w,p;
  ((w | w) | (p | w)) = (p | w) | (w | w) by Th83;
  hence thesis by Th121;
end;

theorem Th134:
  for p,y,w holds (w | (y | (y | y))) | (w | p) = w
proof
  let p,y,w;
  (w | w) = (w | (y | (y | y))) by SHEFFER1:def 14;
  hence thesis by Th132;
end;

theorem Th135:
  for p,w holds ((w | p) | (w | w)) = w
proof
  let p,w;
  ((w | w) | (w | p)) = ((w | p) | (w | w)) by Th83;
  hence thesis by Th132;
end;

theorem Th136:
  for y,p,w holds (w | p) | (w | (y | (y | y))) = w
proof
  let y,p,w;
  w | w = (w | (y | (y | y))) by SHEFFER1:def 14;
  hence thesis by Th135;
end;

theorem Th137:
  for p,q,w,y,x holds ((((x | (y | (y | y))) | w) | ((q | q) | w)
) | ((w | (x | q)) | (w | (x | q)))) = (((w | (p | (p | p))) | (w | (x | q))) |
  (((x | q) | (x | q)) | (w | (x | q))))
proof
  let p,q,w,y,x;
  ((w | (x | q)) | (w | (x | q))) = (((x | (y | (y | y))) | w) | ((q | q)
  | w)) by Th73;
  hence thesis by Th73;
end;

theorem Th138:
  for q,w,y,x holds ((((x | (y | (y | y))) | w) | ((q | q) | w))
| ((w | (x | q)) | (w | (x | q)))) = (w | (((x | q) | (x | q)) | (w | (x | q)))
  )
proof
  now
    let y,p,w,q,x;
    ((w | (p | (p | p))) | (w | (x | q))) = w by Th134;
    hence ((((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w |
    (x | q)))) = (w | (((x | q) | (x | q)) | (w | (x | q)))) by Th137;
  end;
  hence thesis;
end;

theorem Th139:
  for q,w,y,x holds (((x | (y | (y | y))) | w) | ((q | q) | w)) |
  ((w | (x | q)) | (w | (x | q))) = w | (x | q)
proof
  let q,w,y,x;
  ((x | q) | (x | q)) | (w | (x | q)) = x | q by Th121;
  hence thesis by Th138;
end;

theorem Th140:
  for z,p,q,y,x holds ((((x | (y | (y | y))) | q) | ((z | z) | q)
) | ((q | (x | z)) | (q | (x | z)))) = ((((z | z) | (p | (p | p))) | ((x | (y |
  (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q)))
proof
  let z,p,q,y,x;
  (((x | (y | (y | y))) | q) | ((z | z) | q)) = ((q | (x | z)) | (q | (x |
  z))) by Th73;
  hence thesis by Th73;
end;

theorem Th141:
  for z,p,q,y,x holds q | (x | z) = (((z | z) | (p | (p | p))) |
  ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q))
proof
  let z,p,q,y,x;
  ((((x | (y | (y | y))) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x
  | z)))) = (q | (x | z)) by Th139;
  hence thesis by Th140;
end;

theorem Th142:
  for z,q,y,x holds q | (x | z) = (z | ((x | (y | (y | y))) | q))
  | ((q | q) | ((x | (y | (y | y))) | q))
proof
  now
    let p,z,q,y,x;
    (z | z) | (p | (p | p)) = z by Th71;
    hence
    (q | (x | z)) = ((z | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (
    y | (y | y))) | q))) by Th141;
  end;
  hence thesis;
end;

theorem Th143:
  for v,p,y,x holds p | (x | v) = (v | ((x | (y | (y | y))) | p)) | p
proof
  let v,p,y,x;
  (p | p) | ((x | (y | (y | y))) | p) = p by Th121;
  hence thesis by Th142;
end;

theorem Th144:
  for y,w,z,v,x holds ((w | (z | (x | v))) | (((x | (y | (y | y))
  ) | z) | ((v | v) | z))) = z | (x | v)
proof
  let y,w,z,v,x;
  (z | (x | v)) | (z | (x | v)) = ((x | (y | (y | y))) | z) | ((v | v) | z
  ) by Th73;
  hence thesis by Th133;
end;

theorem Th145:
  for y,z,x holds ((y | ((x | x) | z)) | (y | ((x | x) | z))) | (
  (x | y) | ((z | z) | y)) = y | ((x | x) | z)
proof
  let y,z,x;
  (y | ((x | x) | z)) | (y | ((x | x) | z)) = (x | y) | ((z | z) | y) by Th74;
  hence thesis by Th121;
end;

theorem Th146:
  for z,y,x holds (z | (x | y)) | y = y | ((x | x) | z)
proof
  let z,y,x;
  (((y | ((x | x) | z)) | (y | ((x | x) | z))) | ((x | y) | ((z | z) | y))
  ) = ((z | (x | y)) | y) by Th123;
  hence thesis by Th145;
end;

theorem Th147:
  for x,w,y,z holds ((((x | x) | w) | ((z | (y | (y | y))) | w))
  | w) = w | (x | z)
proof
  let x,w,y,z;
  (w | (x | z)) | (w | (x | z)) = ((x | x) | w) | ((z | (y | (y | y))) | w
  ) by Th75;
  hence thesis by Th131;
end;

theorem Th148:
  for z,w,x holds (w | (z | ((x | x) | w))) = w | (x | z)
proof
  now
    let x,w,p,z;
    ((((x | x) | w) | ((z | (p | (p | p))) | w)) | w) = w | (z | ((x | x)
    | w)) by Th143;
    hence w | (z | ((x | x) | w)) = w | (x | z) by Th147;
  end;
  hence thesis;
end;

theorem Th149:
  for p,z,y,x holds (((z | (x | p)) | (z | (x | p))) | (((x | (y
| (y | y))) | z) | ((p | p) | z))) = ((((p | p) | z) | ((x | (y | (y | y))) | z
  )) | (((p | p) | z) | ((x | (y | (y | y))) | z)))
proof
  let p,z,y,x;
  (((x | (y | (y | y))) | z) | ((p | p) | z)) = ((z | (x | p)) | (z | (x |
  p))) by Th73;
  hence thesis by Th87;
end;

theorem Th150:
  for p,z,y,x holds (z | (x | p)) = ((((p | p) | z) | ((x | (y |
  (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z)))
proof
  let p,z,y,x;
  (((z | (x | p)) | (z | (x | p))) | (((x | (y | (y | y))) | z) | ((p | p)
  | z))) = z | (x | p) by Th144;
  hence thesis by Th149;
end;

theorem Th151:
  for z,p,y,x holds z | (x | p) = z | (p | ((x | (y | (y | y))) |
  (x | (y | (y | y)))))
proof
  let z,p,y,x;
  (((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y
  | (y | y))) | z)) = z | (p | ((x | (y | (y | y))) | (x | (y | (y | y))))) by
Th130;
  hence thesis by Th150;
end;

theorem Th152:
  for z,p,x holds z | (x | p) = z | (p | x)
proof
  now
    let y,z,p,x;
    (x | (y | (y | y))) | (x | (y | (y | y))) = x by Th136;
    hence z | (x | p) = z | (p | x) by Th151;
  end;
  hence thesis;
end;

theorem Th153:
  for w,q,p holds (p | q) | w = w | (q | p)
proof
  let w,q,p;
  w | (p | q) = (p | q) | w by Th83;
  hence thesis by Th152;
end;

theorem Th154:
  for w,p,q holds ((q | p) | w) | q = q | ((p | p) | w)
proof
  let w,p,q;
  w | (p | q) = (q | p) | w by Th153;
  hence thesis by Th146;
end;

theorem Th155:
  for z,w,y,x holds w | x = (w | ((x | z) | (((x | (y | (y | y)))
  | (x | (y | (y | y)))) | w)))
proof
  let z,w,y,x;
  (x | (y | (y | y))) | (x | z) = x by Th134;
  hence thesis by Th148;
end;

theorem Th156:
  for w,z,x holds w | x = w | ((x | z) | (x | w))
proof
  now
    let y,w,z,x;
    (x | (y | (y | y))) | (x | (y | (y | y))) = x by Th136;
    hence w | x = w | ((x | z) | (x | w)) by Th155;
  end;
  hence thesis;
end;

theorem Th157:
  for q,x,z,y holds ((x | y) | (((x | (y | (z | (z | z)))) | q) |
  x)) = ((x | y) | (x | (y | (z | (z | z)))))
proof
  let q,x,z,y;
  (x | (y | (z | (z | z)))) | (x | y) = x by Th113;
  hence thesis by Th156;
end;

theorem Th158:
  for x,q,z,y holds ((x | y) | (x | (((y | (z | (z | z))) | (y |
  (z | (z | z)))) | q))) = ((x | y) | (x | (y | (z | (z | z)))))
proof
  let x,q,z,y;
  (((x | (y | (z | (z | z)))) | q) | x) = (x | (((y | (z | (z | z))) | (y
  | (z | (z | z)))) | q)) by Th154;
  hence thesis by Th157;
end;

theorem Th159:
  for z,x,q,y holds (x | y) | (x | (y | q)) = ((x | y) | (x | (y
  | (z | (z | z)))))
proof
  let z,x,q,y;
  ((y | (z | (z | z))) | (y | (z | (z | z)))) = y by Th136;
  hence thesis by Th158;
end;

theorem Th160:
  for x,q,y holds (x | y) | (x | (y | q)) = x
proof
  now
    let q,x,z,y;
    (x | y) | (x | (y | (z | (z | z)))) = x by Th112;
    hence (x | y) | (x | (y | q)) = x by Th159;
  end;
  hence thesis;
end;

theorem Th161:
  L is satisfying_Sh_1
proof
  given a, b, c being Element of L such that
A1: (a | ((b | a) | a)) | (b | (c | a)) <> b;
A2: a | ((b | a) | a) = b | a by Th126;
  not ((a | ((b | a) | a)) | (b | (a | c))) = b by A1,Th83;
  hence thesis by A2,Th160;
end;

registration
  cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ->
    satisfying_Sh_1 for non empty ShefferStr;
  coherence by Th161;
  cluster satisfying_Sh_1 -> satisfying_Sheffer_1 satisfying_Sheffer_2
    satisfying_Sheffer_3 for non empty ShefferStr;
  coherence by Th67,Th68,Th69;
end;

registration
  cluster satisfying_Sh_1 properly_defined -> Boolean Lattice-like for
non empty
    ShefferOrthoLattStr;
  coherence;
  cluster Boolean Lattice-like well-complemented properly_defined ->
    satisfying_Sh_1 for non empty ShefferOrthoLattStr;
  coherence;
end;