SHEFFER1

:: Axiomatization of {B}oolean Algebras Based on Sheffer Stroke
::  by Violetta Kozarkiewicz 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 LATTICES, ROBBINS1, XBOOLE_0, SUBSET_1, ARYTM_3, EQREL_1,
      STRUCT_0, BINOP_1, FUNCT_5, RELAT_1, FUNCT_1, SHEFFER1, CARD_1;
 notations TARSKI, XBOOLE_0, FUNCT_5, ORDINAL1, CARD_1, STRUCT_0, LATTICES,
      BINOP_1, ROBBINS1;
 constructors BINOP_1, ROBBINS1, FUNCT_5;
 registrations LATTICES, LATTICE6, ROBBINS1, CARD_1, STRUCT_0;
 definitions LATTICES, ROBBINS1, STRUCT_0;
 equalities ROBBINS1;
 expansions LATTICES, ROBBINS1, STRUCT_0;
 theorems STRUCT_0, ROBBINS1, LATTICES;

begin :: Preliminaries

theorem Th1:
  for L being join-commutative join-associative Huntington non
  empty ComplLLattStr, a, b being Element of L holds (a + b)` = a` *' b`
proof
  let L be join-commutative join-associative Huntington non empty
  ComplLLattStr;
  let a, b be Element of L;
  a + b = (a` *' b`)` by ROBBINS1:17;
  hence thesis by ROBBINS1:3;
end;

begin :: Huntington's First Axiomatization of Boolean Algebras

definition
  let IT be non empty LattStr;
  attr IT is upper-bounded' means

  ex c being Element of IT st for a
  being Element of IT holds c "/\" a = a & a "/\" c = a;
end;

definition
  let L be non empty LattStr;
  assume
A1: L is upper-bounded';
  func Top' L -> Element of L means
  :Def2:
  for a being Element of L holds it "/\" a = a & a "/\" it = a;
  existence by A1;
  uniqueness
  proof
    let c1,c2 be Element of L such that
A2: for a being Element of L holds c1"/\"a = a & a"/\"c1 = a and
A3: for a being Element of L holds c2"/\"a = a & a"/\"c2 = a;
    thus c1 = c2"/\"c1 by A3
      .= c2 by A2;
  end;
end;

definition
  let IT be non empty LattStr;
  attr IT is lower-bounded' means

  ex c being Element of IT st for a
  being Element of IT holds c "\/" a = a & a "\/" c = a;
end;

definition
  let L be non empty LattStr;
  assume
A1: L is lower-bounded';
  func Bot' L -> Element of L means
  :Def4:
  for a being Element of L holds it "\/" a = a & a "\/" it = a;
  existence by A1;
  uniqueness
  proof
    let c1,c2 be Element of L such that
A2: for a being Element of L holds c1"\/"a = a & a"\/"c1 = a and
A3: for a being Element of L holds c2"\/"a = a & a"\/"c2 = a;
    thus c1 = c2"\/"c1 by A3
      .= c2 by A2;
  end;
end;

definition
  let IT be non empty LattStr;
  attr IT is distributive' means
  :Def5:
  for a, b, c being Element of IT holds
  a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c);
end;

definition
  let L be non empty LattStr, a, b be Element of L;
  pred a is_a_complement'_of b means

  b "\/" a = Top' L & a "\/" b = Top' L &
  b "/\" a = Bot' L & a "/\" b = Bot' L;
end;

definition
  let IT be non empty LattStr;
  attr IT is complemented' means
  :Def7:
  for b being Element of IT ex a being
  Element of IT st a is_a_complement'_of b;
end;

definition
  let L be non empty LattStr, x be Element of L;
  assume
A1: L is complemented' distributive upper-bounded' meet-commutative;
  func x `# -> Element of L means
  :Def8:
  it is_a_complement'_of x;
  existence by A1;
  uniqueness
  proof
    let a,b be Element of L such that
A2: a is_a_complement'_of x and
A3: b is_a_complement'_of x;
    b = b "/\" Top' L by A1,Def2
      .= b "/\" (x "\/" a) by A2
      .= (b "/\" x) "\/" (b "/\" a) by A1
      .= (x "/\" b) "\/" (b "/\" a) by A1
      .= (x "/\" b) "\/" (a "/\" b) by A1
      .= (Bot' L) "\/" (a "/\" b) by A3
      .= (a "/\" x) "\/" (a "/\" b) by A2
      .= a "/\" (x "\/" b) by A1
      .= a "/\" Top' L by A3
      .= a by A1,Def2;
    hence thesis;
  end;
end;

registration
  cluster Boolean join-idempotent upper-bounded' complemented' distributive'
    lower-bounded' Lattice-like for 1-element LattStr;
  existence
  proof
    set L = the 1-element Lattice;
A1: L is lower-bounded
    proof
      set x = the Element of L;
      for y be Element of L holds x "/\" y = x & y "/\" x = x by
STRUCT_0:def 10;
      hence thesis;
    end;
A2: L is upper-bounded
    proof
      set x = the Element of L;
      for y be Element of L holds x "\/" y = x & y "\/" x = x by
STRUCT_0:def 10;
      hence thesis;
    end;
    for b being Element of L ex a being Element of L st a is_a_complement_of b
    proof
      let b be Element of L;
      take a = b;
      b "\/" a = Top L & b "/\" a = Bottom L by STRUCT_0:def 10;
      hence thesis;
    end;
    then
A3: L is complemented;
A4: L is join-idempotent;
    for b being Element of L ex a being Element of L st a is_a_complement'_of b
    proof
      let b be Element of L;
      take a = b;
      b "\/" a = Top' L & b "/\" a = Bot' L by STRUCT_0:def 10;
      hence thesis;
    end;
    then
A5: L is complemented';
    for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b)
    "\/" (a "/\" c) by STRUCT_0:def 10;
    then
A6: L is distributive;
A7: L is lower-bounded'
    proof
      set x = the Element of L;
      for y be Element of L holds x "\/" y = y & y "\/" x = y by
STRUCT_0:def 10;
      hence thesis;
    end;
A8: L is upper-bounded'
    proof
      set x = the Element of L;
      for y be Element of L holds x "/\" y = y & y "/\" x = y by
STRUCT_0:def 10;
      hence thesis;
    end;
    for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b)
    "/\" (a "\/" c) by STRUCT_0:def 10;
    then L is distributive';
    hence thesis by A3,A6,A1,A2,A4,A8,A5,A7;
  end;
end;

theorem Th2:
  for L being complemented' join-commutative meet-commutative
distributive upper-bounded' distributive' non empty LattStr for x be Element
  of L holds x "\/" x `# = Top' L
proof
  let L be complemented' join-commutative meet-commutative distributive
  upper-bounded' distributive' non empty LattStr;
  let x be Element of L;
  x `# is_a_complement'_of x by Def8;
  hence thesis;
end;

theorem Th3:
  for L being complemented' join-commutative meet-commutative
  distributive upper-bounded' distributive' non empty LattStr for x being
  Element of L holds x "/\" x `# = Bot' L
proof
  let L be complemented' join-commutative meet-commutative distributive
  upper-bounded' distributive' non empty LattStr;
  let x be Element of L;
  x `# is_a_complement'_of x by Def8;
  hence thesis;
end;

theorem Th4:
  for L being complemented' join-commutative meet-commutative
  join-idempotent distributive upper-bounded' distributive' non empty LattStr
  for x being Element of L holds x "\/" Top' L = Top' L
proof
  let L be complemented' join-commutative meet-commutative join-idempotent
  distributive upper-bounded' distributive' non empty LattStr;
  let x be Element of L;
  x "\/" Top' L = (x "\/" Top' L) "/\" Top' L by Def2
    .= (x "\/" Top' L) "/\" (x "\/" (x `# )) by Th2
    .= x "\/" (Top' L "/\" x`# ) by Def5
    .= x "\/" x `# by Def2
    .= Top' L by Th2;
  hence thesis;
end;

theorem Th5:
  for L being complemented' join-commutative meet-commutative
  join-idempotent distributive upper-bounded' lower-bounded' distributive' non
  empty LattStr for x being Element of L holds x "/\" Bot' L = Bot' L
proof
  let L be complemented' join-commutative meet-commutative join-idempotent
  distributive upper-bounded' lower-bounded' distributive' non empty LattStr;
  let x be Element of L;
  x "/\" Bot' L = (x "/\" Bot' L) "\/" Bot' L by Def4
    .= (x "/\" Bot' L) "\/" (x "/\" x`# ) by Th3
    .= x "/\" (Bot' L "\/" x`# ) by LATTICES:def 11
    .= x "/\" x`# by Def4
    .= Bot' L by Th3;
  hence thesis;
end;

theorem Th6:
  for L being join-commutative meet-absorbing meet-commutative
  join-absorbing join-idempotent distributive non empty LattStr for x, y, z
  being Element of L holds ((x "\/" y) "\/" z) "/\" x = x
proof
  let L be join-commutative meet-absorbing meet-commutative join-absorbing
  join-idempotent distributive non empty LattStr;
  let x, y, z be Element of L;
  ((x "\/" y) "\/" z) "/\" x = (x "/\" (x "\/" y)) "\/" (x "/\" z) by
LATTICES:def 11
    .= (x "/\" x) "\/" (x "/\" y) "\/" (x "/\" z) by LATTICES:def 11
    .= x "\/" (x "/\" y) "\/" (x "/\" z)
    .= x "\/" (x "/\" z) by LATTICES:def 8
    .= x by LATTICES:def 8;
  hence thesis;
end;

theorem Th7:
  for L being join-commutative meet-absorbing meet-commutative
  join-absorbing join-idempotent distributive' non empty LattStr for x, y, z
  being Element of L holds ((x "/\" y) "/\" z) "\/" x = x
proof
  let L be join-commutative meet-absorbing meet-commutative join-absorbing
  join-idempotent distributive' non empty LattStr;
  let x, y, z be Element of L;
  ((x "/\" y) "/\" z) "\/" x = (x "\/" (x "/\" y)) "/\" (x "\/" z) by Def5
    .= (x "\/" x) "/\" (x "\/" y) "/\" (x "\/" z) by Def5
    .= x "/\" (x "\/" y) "/\" (x "\/" z)
    .= x "/\" (x "\/" z) by LATTICES:def 9
    .= x by LATTICES:def 9;
  hence thesis;
end;

definition
  let G be non empty /\-SemiLattStr;
  attr G is meet-idempotent means

  for x being Element of G holds x "/\" x = x;
end;

theorem Th8:
  for L being complemented' join-commutative meet-commutative
  distributive upper-bounded' lower-bounded' distributive' non empty LattStr
  holds L is meet-idempotent
proof
  let L be complemented' join-commutative meet-commutative distributive
  upper-bounded' lower-bounded' distributive' non empty LattStr;
  now
    let x be Element of L;
    thus x "/\" x = (x "/\" x) "\/" Bot' L by Def4
      .= (x "/\" x) "\/" (x "/\" x`# ) by Th3
      .= x "/\" (x "\/" x`# ) by LATTICES:def 11
      .= x "/\" Top' L by Th2
      .= x by Def2;
  end;
  hence thesis;
end;

theorem Th9:
  for L being complemented' join-commutative meet-commutative
  distributive upper-bounded' lower-bounded' distributive' non empty LattStr
  holds L is join-idempotent
proof
  let L be complemented' join-commutative meet-commutative distributive
  upper-bounded' lower-bounded' distributive' non empty LattStr;
  let x be Element of L;
  thus x "\/" x = (x "\/" x) "/\" Top' L by Def2
    .= (x "\/" x) "/\" (x "\/" x`# ) by Th2
    .= x "\/" (x "/\" x`# ) by Def5
    .= x "\/" Bot' L by Th3
    .= x by Def4;
end;

theorem Th10:
  for L being complemented' join-commutative meet-commutative
  join-idempotent distributive upper-bounded' distributive' non empty LattStr
  holds L is meet-absorbing
proof
  let L be complemented' join-commutative meet-commutative join-idempotent
  distributive upper-bounded' distributive' non empty LattStr;
  let y, x be Element of L;
  x "\/" (x "/\" y) = (Top' L "/\" x) "\/" (x "/\" y) by Def2
    .= x "/\" (Top' L "\/" y) by LATTICES:def 11
    .= x "/\" Top' L by Th4
    .= x by Def2;
  hence thesis;
end;

theorem Th11:
  for L being complemented' join-commutative upper-bounded'
meet-commutative join-idempotent distributive distributive' lower-bounded' non
  empty LattStr holds L is join-absorbing
proof
  let L be complemented' join-commutative upper-bounded' meet-commutative
join-idempotent distributive distributive' lower-bounded' non empty LattStr;
  let x, y be Element of L;
A1: L is meet-idempotent by Th8;
A2: L is meet-absorbing by Th10;
  x "/\" (x "\/" y) = (x "/\" x) "\/" (x "/\" y) by LATTICES:def 11
    .= x "\/" (x "/\" y) by A1
    .= x by A2;
  hence thesis;
end;

theorem Th12:
  for L being complemented' join-commutative meet-commutative
  upper-bounded' lower-bounded' join-idempotent distributive distributive' non
  empty LattStr holds L is upper-bounded
proof
  let L be complemented' join-commutative meet-commutative upper-bounded'
lower-bounded' join-idempotent distributive distributive' non empty LattStr;
  ex c being Element of L st for a being Element of L holds c"\/"a = c & a
  "\/"c = c
  proof
    take Top' L;
    let a be Element of L;
    thus thesis by Th4;
  end;
  hence thesis;
end;

theorem Th13:
  for L being Boolean Lattice-like non empty LattStr holds L is
  upper-bounded'
proof
  let L be Boolean Lattice-like non empty LattStr;
  ex c being Element of L st for a being Element of L holds c "/\" a = a &
  a "/\" c = a
  proof
    take c = Top L;
    let a be Element of L;
    thus thesis;
  end;
  hence thesis;
end;

theorem Th14:
  for L being complemented' join-commutative meet-commutative
  upper-bounded' lower-bounded' join-idempotent distributive distributive' non
  empty LattStr holds L is lower-bounded
proof
  let L be complemented' join-commutative meet-commutative upper-bounded'
lower-bounded' join-idempotent distributive distributive' non empty LattStr;
  ex c being Element of L st for a being Element of L holds c"/\"a = c & a
  "/\"c = c
  proof
    take Bot' L;
    let a be Element of L;
    thus thesis by Th5;
  end;
  hence thesis;
end;

theorem Th15:
  for L being Boolean Lattice-like non empty LattStr holds L is
  lower-bounded'
proof
  let L be Boolean Lattice-like non empty LattStr;
  ex c being Element of L st for a being Element of L holds c "\/" a = a &
  a "\/" c = a
  proof
    take c = Bottom L;
    let a be Element of L;
    thus thesis;
  end;
  hence thesis;
end;

theorem Th16:
  for L being join-commutative meet-commutative meet-absorbing
  join-absorbing join-idempotent distributive non empty LattStr holds L is
  join-associative
proof
  let L be join-commutative meet-commutative meet-absorbing join-absorbing
  join-idempotent distributive non empty LattStr;
  let x, y, z be Element of L;
A1: ((y "\/" z) "\/" x) "/\" y = (y "/\" (y "\/" z)) "\/" (y "/\" x) by
LATTICES:def 11
    .= (y "/\" y) "\/" (y "/\" z) "\/" (y "/\" x) by LATTICES:def 11
    .= y "\/" (y "/\" z) "\/" (y "/\" x)
    .= y "\/" (y "/\" x) by LATTICES:def 8
    .= y by LATTICES:def 8;
A2: ((x "\/" y) "\/" z) "/\" x = x by Th6;
  x "\/" (y "\/" z) = (x "\/" y) "\/" z
  proof
    set A = ((x "\/" y) "\/" z) "/\" (x "\/" (y "\/" z));
A3: A = ((x "\/" y) "/\" (x "\/" (y "\/" z))) "\/" (z "/\" (x "\/" (y "\/"
    z))) by LATTICES:def 11
      .= ((x "\/" y) "/\" (x "\/" (y "\/" z))) "\/" z by Th6
      .= ((x "/\" (x "\/" (y "\/" z))) "\/" (y "/\" (x "\/" (y "\/" z))))
    "\/" z by LATTICES:def 11
      .= (x "\/" y) "\/" z by A1,LATTICES:def 9;
    A = (((x "\/" y) "\/" z) "/\" x) "\/" (((x "\/" y) "\/" z) "/\" (y
    "\/" z)) by LATTICES:def 11
      .= x "\/" ((((x "\/" y) "\/" z) "/\" y) "\/" (((x "\/" y) "\/" z) "/\"
    z)) by A2,LATTICES:def 11
      .= x "\/" (y "\/" (((x "\/" y) "\/" z) "/\" z)) by Th6
      .= x "\/" (y "\/" (((x "\/" y ) "/\" z) "\/" (z "/\" z))) by
LATTICES:def 11
      .= x "\/" (y "\/" (((x "\/" y ) "/\" z) "\/" z))
      .= x "\/" (y "\/" z) by LATTICES:def 8;
    hence thesis by A3;
  end;
  hence thesis;
end;

theorem Th17:
  for L being join-commutative meet-commutative meet-absorbing
  join-absorbing join-idempotent distributive' non empty LattStr holds L is
  meet-associative
proof
  let L be join-commutative meet-commutative meet-absorbing join-absorbing
  join-idempotent distributive' non empty LattStr;
  let x, y, z be Element of L;
A1: ((x "/\" y) "/\" z) "\/" x = x by Th7;
A2: ((y "/\" z) "/\" x) "\/" y = (y "\/" (y "/\" z)) "/\" (y "\/" x) by Def5
    .= (y "\/" y) "/\" (y "\/" z) "/\" (y "\/" x) by Def5
    .= y "/\" (y "\/" z) "/\" (y "\/" x)
    .= y "/\" (y "\/" x) by LATTICES:def 9
    .= y by LATTICES:def 9;
  x "/\" (y "/\" z) = (x "/\" y) "/\" z
  proof
    set A = ((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z));
A3: A = ((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" (z "\/" (x "/\" (y "/\"
    z))) by Def5
      .= ((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" z by Th7
      .= ((x "\/" (x "/\" (y "/\" z))) "/\" (y "\/" (x "/\" (y "/\" z))))
    "/\" z by Def5
      .= (x "/\" y) "/\" z by A2,LATTICES:def 8;
    A = (((x "/\" y) "/\" z) "\/" x) "/\" (((x "/\" y) "/\" z) "\/" (y
    "/\" z)) by Def5
      .= x "/\" ((((x "/\" y) "/\" z) "\/" y) "/\" (((x "/\" y) "/\" z) "\/"
    z)) by A1,Def5
      .= x "/\" (y "/\" (((x "/\" y) "/\" z) "\/" z)) by Th7
      .= x "/\" (y "/\" (((x "/\" y ) "\/" z) "/\" (z "\/" z))) by Def5
      .= x "/\" (y "/\" (((x "/\" y ) "\/" z) "/\" z))
      .= x "/\" (y "/\" z) by LATTICES:def 9;
    hence thesis by A3;
  end;
  hence thesis;
end;

theorem Th18:
  for L being complemented' join-commutative meet-commutative
  lower-bounded' upper-bounded' join-idempotent distributive distributive' non
  empty LattStr holds Top L = Top' L
proof
  let L be complemented' join-commutative meet-commutative lower-bounded'
upper-bounded' join-idempotent distributive distributive' non empty LattStr;
  set Y = Top' L;
  L is upper-bounded & for a being Element of L holds Y "\/" a = Y & a
  "\/" Y = Y by Th4,Th12;
  hence thesis by LATTICES:def 17;
end;

theorem Th19:
  for L being complemented' join-commutative meet-commutative
  lower-bounded' upper-bounded' join-idempotent distributive distributive' non
  empty LattStr holds Bottom L = Bot' L
proof
  let L be complemented' join-commutative meet-commutative lower-bounded'
upper-bounded' join-idempotent distributive distributive' non empty LattStr;
  set Y = Bot' L;
  L is lower-bounded & for a being Element of L holds Y "/\" a = Y & a
  "/\" Y = Y by Th5,Th14;
  hence thesis by LATTICES:def 16;
end;

theorem Th20:
  for L being Boolean distributive' Lattice-like non empty
  LattStr holds Top L = Top' L
proof
  let L be Boolean distributive' Lattice-like non empty LattStr;
  set Y = Top L;
  L is upper-bounded' & for a being Element of L holds Y "/\" a = a & a
  "/\" Y = a by Th13;
  hence thesis by Def2;
end;

theorem Th21:
  for L being Boolean complemented lower-bounded upper-bounded
  distributive distributive' Lattice-like non empty LattStr holds Bottom L =
  Bot' L
proof
  let L be Boolean complemented lower-bounded upper-bounded distributive
  distributive' Lattice-like non empty LattStr;
  set Y = Bottom L;
  L is lower-bounded' & for a being Element of L holds Y "\/" a = a & a
  "\/" Y = a by Th15;
  hence thesis by Def4;
end;

theorem
  for L being complemented' lower-bounded' upper-bounded'
  join-commutative meet-commutative join-idempotent distributive distributive'
  non empty LattStr, x, y being Element of L holds
  x is_a_complement'_of y iff x is_a_complement_of y
by Th19,Th18;

theorem Th23:
  for L being complemented' join-commutative meet-commutative
  lower-bounded' upper-bounded' join-idempotent distributive distributive' non
  empty LattStr holds L is complemented
proof
  let L be complemented' join-commutative meet-commutative lower-bounded'
upper-bounded' join-idempotent distributive distributive' non empty LattStr;
  for b being Element of L ex a being Element of L st a is_a_complement_of b
  proof
    let b be Element of L;
    consider a being Element of L such that
A1: a is_a_complement'_of b by Def7;
    take a;
A2: b "/\" a = Bot' L by A1;
    b "\/" a = Top' L by A1;
    hence a"\/"b = Top L & b"\/"a = Top L &
    a"/\"b = Bottom L & b"/\"a = Bottom L by A2,Th18,Th19;
  end;
  hence thesis;
end;

theorem Th24:
  for L being Boolean lower-bounded' upper-bounded' distributive'
  Lattice-like non empty LattStr holds L is complemented'
proof
  let L be Boolean lower-bounded' upper-bounded' distributive' Lattice-like
  non empty LattStr;
  for b being Element of L ex a being Element of L st a is_a_complement'_of b
  proof
    let b be Element of L;
    consider a being Element of L such that
A1: a is_a_complement_of b by LATTICES:def 19;
    take a;
A2: b "/\" a = Bottom L by A1;
    b "\/" a = Top L by A1;
    hence b "\/" a = Top' L & a "\/" b = Top' L &
    b "/\" a = Bot' L & a "/\" b = Bot' L by A2,Th20,Th21;
  end;
  hence thesis;
end;

theorem Th25:
  for L being non empty LattStr holds L is Boolean Lattice iff L
is lower-bounded' upper-bounded' join-commutative meet-commutative distributive
  distributive' complemented'
proof
  let L be non empty LattStr;
  thus L is Boolean Lattice implies L is lower-bounded' upper-bounded'
  join-commutative meet-commutative distributive distributive' complemented'
  proof
    assume
A1: L is Boolean Lattice;
    then reconsider L9 = L as Boolean Lattice;
    ex c being Element of L9 st for a being Element of L9 holds c "\/" a =
    a & a "\/" c = a
    proof
      take Bottom L9;
      thus thesis;
    end;
    hence
A2: L is lower-bounded';
    ex c being Element of L9 st for a being Element of L9 holds c "/\" a =
    a & a "/\" c = a
    proof
      take Top L9;
      thus thesis;
    end;
    hence
A3: L is upper-bounded';
    thus L is join-commutative meet-commutative by A1;
    for a,b,c being Element of L9 holds a "/\" (b "\/" c) = (a "/\" b)
    "\/" (a "/\" c) by LATTICES:def 11;
    then for a, b, c being Element of L9 holds a "\/" (b "/\" c) = (a "\/" b)
    "/\" (a "\/" c) by LATTICES:3;
    hence L is distributive distributive';
    hence thesis by A1,A2,A3,Th24;
  end;
  thus L is lower-bounded' upper-bounded' join-commutative meet-commutative
  distributive distributive' complemented' implies L is Boolean Lattice
  proof
    assume L is lower-bounded' upper-bounded' join-commutative
    meet-commutative distributive distributive' complemented';
    then reconsider L9 = L as lower-bounded' upper-bounded' complemented'
join-commutative meet-commutative join-idempotent distributive distributive'
    non empty LattStr by Th9;
A4: L9 is complemented by Th23;
A5: L9 is lower-bounded & L9 is upper-bounded by Th12,Th14;
A6: L9 is meet-absorbing join-absorbing by Th10,Th11;
    then L9 is join-associative & L9 is meet-associative by Th16,Th17;
    hence thesis by A5,A4,A6;
  end;
end;

registration
  cluster Boolean Lattice-like -> lower-bounded' upper-bounded' complemented'
join-commutative meet-commutative distributive distributive' for
non empty LattStr;
  coherence by Th25;
  cluster lower-bounded' upper-bounded' complemented' join-commutative
meet-commutative distributive distributive' -> Boolean Lattice-like for
non empty
    LattStr;
  coherence by Th25;
end;

begin :: Axiomatization Based on Sheffer Stroke

definition
  struct (1-sorted) ShefferStr (# carrier -> set, stroke -> BinOp of the
    carrier #);
end;

definition
  struct (ShefferStr,LattStr) ShefferLattStr (# carrier -> set, L_join ->
BinOp of the carrier, L_meet -> BinOp of the carrier, stroke -> BinOp of the
    carrier #);
end;

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

definition
  func TrivShefferOrthoLattStr -> ShefferOrthoLattStr equals
  ShefferOrthoLattStr (# {0}, op2, op2, op1, op2 #);
  coherence;
end;

registration
  cluster 1-element for ShefferStr;
  existence
  proof
    set S = {{}};
    set B = the BinOp of S;
    take ShefferStr (#S, B#);
    thus the carrier of ShefferStr (#S, B#) is 1-element;
  end;
  cluster 1-element for ShefferLattStr;
  existence
  proof
    set S = {{}};
    set B = the BinOp of S;
    take ShefferLattStr (#S, B, B, B#);
    thus the carrier of ShefferLattStr (#S, B, B, B#) is 1-element;
  end;
  cluster 1-element for ShefferOrthoLattStr;
  existence
  proof
    set S = {{}};
    set B = the BinOp of S;
    set A = the UnOp of S;
    take ShefferOrthoLattStr (#S, B, B, A, B#);
    thus the carrier of ShefferOrthoLattStr (#S, B, B, A, B#) is 1-element;
  end;
end;

definition
  let L be non empty ShefferStr;
  let x, y be Element of L;
  func x | y -> Element of L equals
  (the stroke of L).(x,y);
  coherence;
end;

definition
  let L be non empty ShefferOrthoLattStr;
  attr L is properly_defined means
  :Def12:
  (for x being Element of L holds x |
x = x`) & (for x, y being Element of L holds x "\/" y = (x | x) | (y | y)) & (
  for x, y being Element of L holds x "/\" y = (x | y) | (x | y)) & for x, y
  being Element of L holds x | y = x` + y`;
end;

definition
  let L be non empty ShefferStr;
  attr L is satisfying_Sheffer_1 means
  :Def13:
  for x being Element of L holds (x | x) | (x | x) = x;
  attr L is satisfying_Sheffer_2 means
  :Def14:
  for x, y being Element of L holds x | (y | (y | y)) = x | x;
  attr L is satisfying_Sheffer_3 means
  :Def15:
  for x, y, z being Element of L
  holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x);
end;

registration
  cluster -> satisfying_Sheffer_1 satisfying_Sheffer_2
    satisfying_Sheffer_3 for 1-element ShefferStr;
  coherence
  by STRUCT_0:def 10;
end;

registration
  cluster  -> join-commutative join-associative
   for 1-element \/-SemiLattStr;
  coherence
  by STRUCT_0:def 10;
  cluster  -> meet-commutative meet-associative
        for 1-element /\-SemiLattStr;
  coherence
  by STRUCT_0:def 10;
end;

registration
  cluster -> join-absorbing meet-absorbing Boolean for 1-element LattStr;
  coherence
  proof
    let L be 1-element LattStr;
    thus L is join-absorbing
    by STRUCT_0:def 10;
A1: L is upper-bounded
    proof
      set c = the Element of L;
      take c;
      let a be Element of L;
      thus thesis by STRUCT_0:def 10;
    end;
    thus L is meet-absorbing
    by STRUCT_0:def 10;
A2: L is lower-bounded
    proof
      set c = the Element of L;
      take c;
      let a be Element of L;
      thus thesis by STRUCT_0:def 10;
    end;
A3: L is complemented
    proof
      set a = the Element of L;
      let b be Element of L;
      take a;
A4:   a "/\" b = Bottom L & b "/\" a = Bottom L by STRUCT_0:def 10;
      a "\/" b = Top L & b "\/" a = Top L by STRUCT_0:def 10;
      hence thesis by A4;
    end;
    L is distributive
    by STRUCT_0:def 10;
    hence thesis by A2,A1,A3;
  end;
end;

registration
  cluster TrivShefferOrthoLattStr -> 1-element;
  coherence;
  cluster TrivShefferOrthoLattStr -> properly_defined well-complemented;
  coherence
  proof
    set L = TrivShefferOrthoLattStr;
A1: ( for x, y being Element of L holds x "/\" y = (x | y) | (x | y))& for
    x, y being Element of L holds x | y = x` + y` by STRUCT_0:def 10;
    ( for x being Element of L holds x | x = x`)& for x, y being Element
    of L holds x "\/" y = (x | x) | (y | y) by STRUCT_0:def 10;
    hence L is properly_defined by A1;
    L is well-complemented
    proof
      let a be Element of L;
      thus a` "\/" a = Top L & a "\/" a` = Top L &
      a` "/\" a = Bottom L & a "/\" a` = Bottom L by STRUCT_0:def 10;
    end;
    hence thesis;
  end;
end;

registration
  cluster properly_defined Boolean well-complemented Lattice-like
    satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for
    non empty ShefferOrthoLattStr;
  existence
  proof
    take TrivShefferOrthoLattStr;
    thus thesis;
  end;
end;

theorem
  for L being properly_defined Boolean well-complemented Lattice-like
  non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_1
proof
  let L be properly_defined Boolean well-complemented Lattice-like non empty
  ShefferOrthoLattStr;
  let x be Element of L;
  x`` = x by ROBBINS1:3;
  then (x | x)` = x by Def12;
  hence thesis by Def12;
end;

theorem
  for L being properly_defined Boolean well-complemented Lattice-like
  non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_2
proof
  let L be properly_defined Boolean well-complemented Lattice-like non empty
  ShefferOrthoLattStr;
  let x, y be Element of L;
  x` + Bot L = x` by ROBBINS1:13;
  then x` + (y`` *' y`) = x` by ROBBINS1:15;
  then x` + (y` + y)` = x` by Th1;
  then x | (y` + y) = x` by Def12;
  then x | (y` + y``) = x` by ROBBINS1:3;
  then x | (y | (y`)) = x` by Def12;
  then x | (y | (y | y)) = x` by Def12
    .= x | x by Def12;
  hence thesis;
end;

theorem
  for L being properly_defined Boolean well-complemented Lattice-like
  non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_3
proof
  let L be properly_defined Boolean well-complemented Lattice-like non empty
  ShefferOrthoLattStr;
  let x, y, z be Element of L;
  x *' (y` + z`) = (y` *' x) + (z` *' x) by ROBBINS1:30;
  then (x` + (y | z)`)` = (y` *' x) + (z` *' x) by Def12;
  then (x | (y | z))` = (y` *' x) + (z` *' x) by Def12;
  then (x | (y | z)) | (x | (y | z)) = (y` *' x) + (z` *' x) by Def12
    .= (y` *' x``) + (z` *' x) by ROBBINS1:3
    .= (y` *' x``) + (z` *' x``) by ROBBINS1:3
    .= (y + x`)` + (z` *' x``) by Th1
    .= (y + x`)` + (z + x`)` by Th1
    .= (y + x`) | (z + x`) by Def12
    .= (y`` + x`) | (z + x`) by ROBBINS1:3
    .= (y`` + x`) | (z`` + x`) by ROBBINS1:3
    .= (y` | x) | (z`` + x`) by Def12
    .= (y` | x) | (z` | x) by Def12
    .= ((y | y) | x) | (z` | x) by Def12
    .= ((y | y) | x) | ((z | z) | x) by Def12;
  hence thesis;
end;

definition
  let L be non empty ShefferStr;
  let a be Element of L;
  func a" -> Element of L equals
  a | a;
  coherence;
end;

theorem
  for L being satisfying_Sheffer_3 non empty ShefferOrthoLattStr, x, y
  , z being Element of L holds (x | (y | z))" = (y" | x) | (z" | x) by Def15;

theorem
  for L being satisfying_Sheffer_1 non empty ShefferOrthoLattStr, x
  being Element of L holds x = (x")" by Def13;

theorem Th31:
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr, x, y
  being Element of L holds x | y = y | x
proof
  let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
  properly_defined non empty ShefferOrthoLattStr;
  let x, y be Element of L;
  x | y = ((x | y)")" by Def13
    .= ((x | (y")")")" by Def13
    .= (((y")" |x)")" by Def15
    .= ((y | x)")" by Def13
    .= y | x by Def13;
  hence thesis;
end;

theorem Th32:
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr, x, y
  being Element of L holds x | (x | x) = y | (y | y)
proof
  let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
  properly_defined non empty ShefferOrthoLattStr;
  let x, y be Element of L;
  x | (x | x) = ((x | x") | (x | x"))" by Def13
    .= ((x | x") | (y | y"))" by Def14
    .= ((y | y") | (x | (x | x)))" by Th31
    .= ((y | y")")" by Def14
    .= y | (y | y) by Def13;
  hence thesis;
end;

theorem Th33:
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
  is join-commutative
proof
  let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
  properly_defined non empty ShefferOrthoLattStr;
  let x, y be Element of L;
  x "\/" y = x" | (y | y) by Def12
    .= (y | y) | (x | x) by Th31
    .= y "\/" x by Def12;
  hence thesis;
end;

theorem Th34:
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
  is meet-commutative
proof
  let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
  properly_defined non empty ShefferOrthoLattStr;
  let x, y be Element of L;
  x "/\" y = (x | y) | (x | y) by Def12
    .= (y | x) | (x | y) by Th31
    .= (y | x) | (y | x) by Th31
    .= y "/\" x by Def12;
  hence thesis;
end;

theorem Th35:
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
  is distributive
proof
  let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
  properly_defined non empty ShefferOrthoLattStr;
  let x, y, z be Element of L;
  set Y = y";
  set Z = z";
  x "/\" (y "\/" z) = x "/\" ((y | y) | (z | z)) by Def12
    .= (x | (Y | Z))" by Def12
    .= (Y" | x) | (Z" | x) by Def15
    .= (y | x) | (Z" | x) by Def13
    .= (y | x) | (z | x) by Def13
    .= (x | y) | (z | x) by Th31
    .= (x | y) | (x | z) by Th31
    .= ((x | y)")" | (x | z) by Def13
    .= ((x | y) | (x | y))" | ((x | z)")" by Def13
    .= ((x "/\" y) | ((x | y) | (x | y))) | (((x | z) | (x | z)) | ((x | z)
  | (x | z))) by Def12
    .= ((x "/\" y) | (x "/\" y)) | (((x | z) | (x | z)) | ((x | z) | (x | z)
  )) by Def12
    .= ((x "/\" y) | (x "/\" y)) | ((x "/\" z) | ((x | z) | (x | z))) by Def12
    .= ((x "/\" y) | (x "/\" y)) | ((x "/\" z) | (x "/\" z)) by Def12
    .= (x "/\" y) "\/" (x "/\" z) by Def12;
  hence thesis;
end;

theorem Th36:
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
  is distributive'
proof
  let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
  properly_defined non empty ShefferOrthoLattStr;
  let x, y, z be Element of L;
  set X = (x | x);
  x "\/" (y "/\" z) = x "\/" ((y | z) | (y | z)) by Def12
    .= X | ((y | z)")" by Def12
    .= X | (y | z) by Def13
    .= ((X |(y | z))")" by Def13
    .= ((y" | X) | (z" | X))" by Def15
    .= ((X | y") | (z" | X))" by Th31
    .= ((X | (y | y)) | (X | z"))" by Th31
    .= (((x "\/" y) | (X | (z | z))) | ((X | (y | y)) | (X | (z | z)))) by
Def12
    .= (((x "\/" y) | (x "\/" z)) | ((X | (y | y)) | (X | (z | z)))) by Def12
    .= (((x "\/" y) | (x "\/" z)) | ((x "\/" y) | (X | (z | z)))) by Def12
    .= (((x "\/" y) | (x "\/" z)) | ((x "\/" y) | (x "\/" z))) by Def12
    .= (x "\/" y) "/\" (x "\/" z) by Def12;
  hence thesis;
end;

theorem
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
  is Boolean Lattice
proof
  let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
  properly_defined non empty ShefferOrthoLattStr;
A1: L is distributive & L is distributive' by Th35,Th36;
  ex c being Element of L st for a being Element of L holds c "/\" a = a &
  a "/\" c = a
  proof
    set b = the Element of L;
    take c = (b|b) | ((b|b)|(b|b));
    let a be Element of L;
    thus c "/\" a = a
    proof
      set X = b";
      c "/\" a = (((b | b) | (X | X)) | a)" by Def12
        .= (a | (X | (X | X)))" by Th31
        .= (a | a)" by Def14
        .= a by Def13;
      hence thesis;
    end;
    thus a "/\" c = a
    proof
      set X = b";
      a "/\" c = (a | ((b | b) | (X | X)))" by Def12
        .= (a | a)" by Def14
        .= a by Def13;
      hence thesis;
    end;
  end;
  then
A2: L is upper-bounded';
  ex c being Element of L st for a being Element of L holds c "\/" a = a &
  a "\/" c = a
  proof
    set b = the Element of L;
    take c = (b | (b | b)) | (b | (b | b));
    let a be Element of L;
    c "\/" a = ((b | (b | b))")" | (a | a) by Def12
      .= ((a | (a | a))")" | (a | a) by Th32
      .= (a | (a | a)) | (a | a) by Def13
      .= (a | a) | (a | (a | a)) by Th31
      .= (a | a) | (a | a) by Def14
      .= a by Def13;
    hence c "\/" a = a;
    a "\/" c = (a | a) | ((b | (b | b))")" by Def12
      .= (a | a) | ((a | (a | a))")" by Th32
      .= (a | a) | (a | (a | a)) by Def13
      .= (a | a) | (a | a) by Def14
      .= a by Def13;
    hence a "\/" c = a;
  end;
  then
A3: L is lower-bounded';
  for b being Element of L ex a being Element of L st a is_a_complement'_of b
  proof
    let b be Element of L;
    set a = b | b;
    take a;
A4: Top' L = (b | b) | ((b | b)|(b | b))
    proof
      set X = (b | b) | ((b | b)|(b | b));
      for a being Element of L holds X "/\" a = a & a "/\" X = a
      proof
        let a be Element of L;
        set Y = b";
        thus X "/\" a = (((b | b) | (Y | Y)) | a)" by Def12
        .= (a | (Y | (Y | Y)))" by Th31
        .= (a | a)" by Def14
        .= a by Def13;
        thus a "/\" X = (a | ((b | b) | (Y | Y)))" by Def12
        .= (a | a)" by Def14
        .= a by Def13;
      end;
      hence thesis by A2,Def2;
    end;
    then
A5: b "\/" a = Top' L by Def12;
A6: Bot' L = (b | (b | b)) | (b | (b | b))
    proof
      set X = (b | (b | b)) | (b | (b | b));
      for a being Element of L holds X "\/" a = a & a "\/" X = a
      proof
        let a be Element of L;
        thus X "\/" a = ((b | (b | b))")" | (a | a) by Def12
          .= ((a | (a | a))")" | (a | a) by Th32
          .= (a | (a | a)) | (a | a) by Def13
          .= (a | a) | (a | (a | a)) by Th31
          .= (a | a) | (a | a) by Def14
          .= a by Def13;
        thus a "\/" X = (a | a) | ((b | (b | b))")" by Def12
          .= (a | a) | ((a | (a | a))")" by Th32
          .= (a | a) | (a | (a | a)) by Def13
          .= (a | a) | (a | a) by Def14
          .= a by Def13;
      end;
      hence thesis by A3,Def4;
    end;
    then
A7: b "/\" a = Bot' L by Def12;
A8: a "\/" b = ((b | b) | (b | b)) | (b | b) by Def12
      .= Top' L by A4,Th31;
    a "/\" b = ((b | b) | b) | ((b | b) | b) by Def12
      .= (b | (b | b)) | ((b | b) | b) by Th31
      .= Bot' L by A6,Th31;
    hence thesis by A8,A5,A7;
  end;
  then
A9: L is complemented';
  L is join-commutative & L is meet-commutative by Th33,Th34;
  hence thesis by A3,A2,A9,A1;
end;