ROBBINS5

:: On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander
::  by Adam Grabowski and Damian Sawicki
:: 
:: Received June 29, 2018
:: Copyright (c) 2018-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, EQREL_1, ROBBINS5, XBOOLE_0, SUBSET_1;
 notations TARSKI, STRUCT_0, LATTICES, BINOP_1, FUNCT_2;
 constructors BINOP_1, LATTICES;
 registrations LATTICES;
 expansions LATTICES;
 theorems LATTICES;

begin :: Preliminaries: Sholander axiomatization

 reserve L for non empty LattStr;
 reserve v64,v65,v66,v67,v103,v3,v102,v101,v100,v2,v1,v0 for Element of L;

definition let L;
  attr L is satisfying_Sholander_1 means
  for v0,v1,v2 holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0);
end;

theorem Lemma1:
L is join-absorbing &
(for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0)))
implies for v0 holds (v0"/\"v0)=v0
proof
assume A2: L is join-absorbing;
assume A3: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0));

A7: for v65,v66 holds v65=((v66"/\"v65)"\/"(v65"/\"v65))
proof let v65,v66;
(v65"/\"(v65"\/"v66))=v65 by A2;
hence thesis by A3;
end;

A11: for v1,v0 holds ((v0"/\"v1)"/\"v1)=(v0"/\"v1)
proof let v1,v0;
((v0"/\"v1)"\/"(v1"/\"v1))=v1 by A7;
hence thesis by A2;
end;

A18: for v65,v64,v0 holds
 ((v0"/\"v64)"\/"(v65"/\"v64))=(v64"/\"(v65"\/"(v0"/\"v64)))
proof let v65,v64,v0;
((v0"/\"v64)"/\"v64)=(v0"/\"v64) by A11;
hence thesis by A3;
end;

A35: for v65,v64,v66 holds (v65"/\"(v66"\/"v64))=(v65"/\"(v66"\/"(v64"/\"v65)))
proof let v65,v64,v66;
((v64"/\"v65)"\/"(v66"/\"v65))=(v65"/\"(v66"\/"v64)) by A3;
hence thesis by A18;
end;

A40: for v64,v0 holds (v64"/\"v64)=(v64"/\"((v0"/\"v64)"\/"v64))
proof let v64,v0;
((v0"/\"v64)"\/"(v64"/\"v64))=v64 by A7;
hence thesis by A35;
end;

A49: for v64,v65 holds ((v64"/\"v64)"\/"((v65"/\"v64)"/\"v64))=(v64"/\"v64)
proof let v64,v65;
(v64"/\"((v65"/\"v64)"\/"v64))=((v64"/\"v64)"\/"((v65"/\"v64)"/\"v64)) by A3;
hence thesis by A40;
end;

A51: for v64,v65 holds ((v64"/\"v64)"\/"(v65"/\"v64))=(v64"/\"v64)
proof let v64,v65;
((v65"/\"v64)"/\"v64)=(v65"/\"v64) by A11;
hence thesis by A49;
end;
let v65;
((v65"/\"v65)"\/"(v65"/\"v65))=v65 by A7;
hence thesis by A51;
end;

theorem JoinIdem:
L is join-absorbing &
(for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0)))
implies for v0 holds v0"\/"v0 = v0
proof
assume A3: L is join-absorbing;
assume A4: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0));
A8: for v65,v66 holds v65=((v66"/\"v65)"\/"(v65"/\"v65))
proof let v65,v66;
(v65"/\"(v65"\/"v66))=v65 by A3;
hence thesis by A4;
end;

A12: for v1,v0 holds ((v0"/\"v1)"/\"v1)=(v0"/\"v1)
proof let v1,v0;
((v0"/\"v1)"\/"(v1"/\"v1))=v1 by A8;
hence thesis by A3;
end;

A15: for v65,v64,v0 holds
 ((v0"/\"v64)"\/"(v65"/\"v64))=(v64"/\"(v65"\/"(v0"/\"v64)))
proof let v65,v64,v0;
((v0"/\"v64)"/\"v64)=(v0"/\"v64) by A12;
hence thesis by A4;
end;

A19: for v65,v64,v66 holds (v65"/\"(v66"\/"v64))=(v65"/\"(v66"\/"(v64"/\"v65)))
proof let v65,v64,v66;
((v64"/\"v65)"\/"(v66"/\"v65))=(v65"/\"(v66"\/"v64)) by A4;
hence thesis by A15;
end;

A24: for v64,v0 holds (v64"/\"v64)=(v64"/\"((v0"/\"v64)"\/"v64))
proof let v64,v0;
((v0"/\"v64)"\/"(v64"/\"v64))=v64 by A8;
hence thesis by A19;
end;

A35: for v64,v1 holds
 ((v64"/\"v64)"\/"(((v1"/\"v64)"\/"v64)"/\"((v1"/\"v64)"\/"v64)))=
   ((v1"/\"v64)"\/"v64)
proof let v64,v1;
(v64"/\"((v1"/\"v64)"\/"v64))=(v64"/\"v64) by A24;
hence thesis by A8;
end;

A42: for v0,v1 holds
 (v0"\/"(((v1"/\"v0)"\/"v0)"/\"((v1"/\"v0)"\/"v0)))=((v1"/\"v0)"\/"v0)
proof let v0,v1;
(v0"/\"v0)=v0 by A3,A4,Lemma1;
hence thesis by A35;
end;

A44: for v0,v1 holds (v0"\/"((v1"/\"v0)"\/"v0))=((v1"/\"v0)"\/"v0)
proof let v0,v1;
(((v1"/\"v0)"\/"v0)"/\"((v1"/\"v0)"\/"v0))=((v1"/\"v0)"\/"v0) by A3,A4,Lemma1;
hence thesis by A42;
end;

A46: for v1,v0 holds ((v0"/\"v1)"\/"v1)=v1
proof let v1,v0;
(v1"/\"v1)=v1 by A3,A4,Lemma1;
hence thesis by A8;
end;

A48: for v0,v1 holds (v0"\/"v0)=((v1"/\"v0)"\/"v0)
proof let v0,v1;
((v1"/\"v0)"\/"v0)=v0 by A46;
hence thesis by A44;
end;

now let v0,v1;
((v1"/\"v0)"\/"v0)=v0 by A46;
hence (v0"\/"v0)=v0 by A48;
end;
hence thesis;
end;

:: Proofs

theorem MeetCom: :: meet-commutative
L is join-absorbing &
(for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0)))
implies for v0,v1 holds v0"/\"v1 = v1"/\"v0
proof
assume A3: L is join-absorbing;
assume A4: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0));
A53: for v2,v0 holds (v0"/\"(v2"\/"v2))=(v2"/\"v0)
proof let v2,v0;
((v2"/\"v0)"\/"(v2"/\"v0))=(v0"/\"(v2"\/"v2)) by A4;
hence thesis by A3,A4,JoinIdem;
end;
let v2,v0;
(v2"\/"v2)=v2 by A3,A4,JoinIdem;
hence thesis by A53;
end;

:: Join-commutativity

theorem JoinCom:
L is join-absorbing &
(for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0)))
implies for v0,v1 holds v0"\/"v1=v1"\/"v0
proof
assume A3: L is join-absorbing;
assume A4: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0));
A8: for v65,v66 holds v65=((v66"/\"v65)"\/"(v65"/\"v65))
proof let v65,v66;
(v65"/\"(v65"\/"v66))=v65 by A3;
hence thesis by A4;
end;

A12: for v1,v0 holds ((v0"/\"v1)"/\"v1)=(v0"/\"v1)
proof let v1,v0;
((v0"/\"v1)"\/"(v1"/\"v1))=v1 by A8;
hence thesis by A3;
end;

A15: for v65,v64,v0 holds
 ((v0"/\"v64)"\/"(v65"/\"v64))=(v64"/\"(v65"\/"(v0"/\"v64)))
proof let v65,v64,v0;
((v0"/\"v64)"/\"v64)=(v0"/\"v64) by A12;
hence thesis by A4;
end;

A19: for v65,v64,v66 holds (v65"/\"(v66"\/"v64))=(v65"/\"(v66"\/"(v64"/\"v65)))
proof let v65,v64,v66;
((v64"/\"v65)"\/"(v66"/\"v65))=(v65"/\"(v66"\/"v64)) by A4;
hence thesis by A15;
end;

A24: for v64,v0 holds (v64"/\"v64)=(v64"/\"((v0"/\"v64)"\/"v64))
proof let v64,v0;
((v0"/\"v64)"\/"(v64"/\"v64))=v64 by A8;
hence thesis by A19;
end;

A29: for v64,v65 holds ((v64"/\"v64)"\/"((v65"/\"v64)"/\"v64))=(v64"/\"v64)
proof let v64,v65;
(v64"/\"((v65"/\"v64)"\/"v64))=((v64"/\"v64)"\/"((v65"/\"v64)"/\"v64)) by A4;
hence thesis by A24;
end;

A31: for v64,v65 holds ((v64"/\"v64)"\/"(v65"/\"v64))=(v64"/\"v64)
proof let v64,v65;
((v65"/\"v64)"/\"v64)=(v65"/\"v64) by A12;
hence thesis by A29;
end;

A42: for v64,v65 holds (v64"/\"(v65"\/"v64))=v64
proof let v64,v65;
((v64"/\"v64)"\/"(v65"/\"v64))=(v64"/\"(v65"\/"v64)) by A4; then
(v64"/\"(v65"\/"v64))=(v64"/\"v64) by A31 .= v64 by A4,A3,Lemma1;
hence thesis;
end;

A46: for v2,v1 holds ((v2"/\"(v1"\/"v2))"\/"(v1"/\"(v1"\/"v2)))=(v1"\/"v2)
proof let v2,v1;
((v1"\/"v2)"/\"(v1"\/"v2))=((v2"/\"(v1"\/"v2))"\/"(v1"/\"(v1"\/"v2))) by A4;
hence thesis by A4,A3,Lemma1;
end;

A48: for v2,v1 holds (v2"\/"(v1"/\"(v1"\/"v2)))=(v1"\/"v2)
proof let v2,v1;
(v2"/\"(v1"\/"v2))=v2 by A42;
hence thesis by A46;
end;
let v1,v2;
(v1"/\"(v1"\/"v2))=v1 by A3;
hence thesis by A48;
end;

:: Meet-associativity

theorem MeetAssoc:
L is join-absorbing &
(for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0)))
implies for v0,v1,v2 holds ((v0"/\"v1)"/\"v2)=(v0"/\"(v1"/\"v2))
proof
assume A2: L is join-absorbing;
assume A3: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0));
A7: for v65,v66 holds v65=((v66"/\"v65)"\/"(v65"/\"v65))
proof let v65,v66;
(v65"/\"(v65"\/"v66))=v65 by A2;
hence thesis by A3;
end;

A11: for v1,v0 holds ((v0"/\"v1)"/\"v1)=(v0"/\"v1)
proof let v1,v0;
((v0"/\"v1)"\/"(v1"/\"v1))=v1 by A7;
hence thesis by A2;
end;

A14: for v1,v64,v2 holds
 (((v2"/\"v64)"\/"(v1"/\"v64))"/\"(v1"\/"v2))=(v64"/\"(v1"\/"v2))
proof let v1,v64,v2;
(v64"/\"(v1"\/"v2))=((v2"/\"v64)"\/"(v1"/\"v64)) by A3;
hence thesis by A11;
end;

A18: for v65,v64,v0 holds
 ((v0"/\"v64)"\/"(v65"/\"v64))=(v64"/\"(v65"\/"(v0"/\"v64)))
proof let v65,v64,v0;
((v0"/\"v64)"/\"v64)=(v0"/\"v64) by A11;
hence thesis by A3;
end;

A22: for v65,v64,v66 holds (v65"/\"(v66"\/"v64))=(v65"/\"(v66"\/"(v64"/\"v65)))
proof let v65,v64,v66;
((v64"/\"v65)"\/"(v66"/\"v65))=(v65"/\"(v66"\/"v64)) by A3;
hence thesis by A18;
end;

A27: for v64,v0 holds (v64"/\"v64)=(v64"/\"((v0"/\"v64)"\/"v64))
proof let v64,v0;
((v0"/\"v64)"\/"(v64"/\"v64))=v64 by A7;
hence thesis by A22;
end;

A32: for v64,v65 holds ((v64"/\"v64)"\/"((v65"/\"v64)"/\"v64))=(v64"/\"v64)
proof let v64,v65;
(v64"/\"((v65"/\"v64)"\/"v64))=((v64"/\"v64)"\/"((v65"/\"v64)"/\"v64)) by A3;
hence thesis by A27;
end;

A34: for v64,v65 holds ((v64"/\"v64)"\/"(v65"/\"v64))=(v64"/\"v64)
proof let v64,v65;
((v65"/\"v64)"/\"v64)=(v65"/\"v64) by A11;
hence thesis by A32;
end;

A55: for v0,v1 holds (v0"\/"(v1"/\"v0))=v0
proof let v0,v1;
(v0"/\"v0)=v0 by A2,A3,Lemma1;
hence thesis by A34;
end;

A57: for v1,v0 holds ((v0"/\"v1)"\/"v1)=v1
proof let v1,v0;
(v1"/\"v1)=v1 by A2,A3,Lemma1;
hence thesis by A7;
end;

A72: for v66,v65,v64 holds
 ((v64"/\"((v64"/\"v65)"\/"(v66"/\"v65)))"\/"
   (v66"/\"((v64"/\"v65)"\/"(v66"/\"v65))))=
(v65"/\"(v66"\/"v64))
proof let v66,v65,v64;
(((v64"/\"v65)"\/"(v66"/\"v65))"/\"(v66"\/"v64))=((v64"/\"((v64"/\"v65)"\/"
(v66"/\"v65)))"\/"(v66"/\"((v64"/\"v65)"\/"(v66"/\"v65)))) by A3;
hence thesis by A14;
end;

A82: for v65,v66 holds ((v66"/\"v65)"/\"(v66"\/"v66))=(v65"/\"(v66"\/"v66))
proof let v65,v66;
((v66"/\"v65)"\/"(v66"/\"v65))=(v66"/\"v65) by JoinIdem,A2,A3;
hence thesis by A14;
end;

A84: for v65,v66 holds ((v66"/\"v65)"/\"v66)=(v65"/\"(v66"\/"v66))
proof let v65,v66;
(v66"\/"v66)=v66 by JoinIdem,A2,A3;
hence thesis by A82;
end;

A86: for v65,v66 holds ((v66"/\"v65)"/\"v66)=(v65"/\"v66)
proof let v65,v66;
(v66"\/"v66)=v66 by JoinIdem,A2,A3;
hence thesis by A84;
end;

A89: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v1"/\"v0)"\/"(v2"/\"v0))
proof let v0,v2,v1;
((v2"/\"v0)"\/"(v1"/\"v0))=(v0"/\"(v1"\/"v2)) by A3;
hence thesis by A2,A3,JoinCom;
end;

A92: for v1,v2,v0 holds
 ((v0"/\"(v1"/\"(v0"\/"v2)))"\/"(v2"/\"((v0"/\"v1)"\/"(v2"/\"v1))))=
   (v1"/\"(v2"\/"v0))
proof let v1,v2,v0;
((v0"/\"v1)"\/"(v2"/\"v1))=(v1"/\"(v0"\/"v2)) by A89;
hence thesis by A72;
end;

A93: for v1,v2,v0 holds
 ((v0"/\"(v1"/\"(v0"\/"v2)))"\/"(v2"/\"(v1"/\"(v0"\/"v2))))=(v1"/\"(v2"\/"v0))
proof let v1,v2,v0;
((v0"/\"v1)"\/"(v2"/\"v1))=(v1"/\"(v0"\/"v2)) by A89;
hence thesis by A92;
end;

A95: for v1,v2,v0 holds ((v1"/\"(v0"\/"v2))"/\"(v0"\/"v2))=(v1"/\"(v2"\/"v0))
proof let v1,v2,v0;
((v0"/\"(v1"/\"(v0"\/"v2)))"\/"(v2"/\"(v1"/\"(v0"\/"v2))))=
((v1"/\"(v0"\/"v2))"/\"(v0"\/"v2)) by A89;
hence thesis by A93;
end;

A97: for v1,v2,v0 holds (v1"/\"(v0"\/"v2))=(v1"/\"(v2"\/"v0))
proof let v1,v2,v0;
((v1"/\"(v0"\/"v2))"/\"(v0"\/"v2))=(v1"/\"(v0"\/"v2)) by A11;
hence thesis by A95;
end;

A101: for v64,v65 holds ((v65"/\"v64)"\/"v65)=v65
proof let v64,v65;
(v64"/\"v65)=(v65"/\"v64) by A2,A3,MeetCom;
hence thesis by A57;
end;

A105: for v65,v64 holds (v64"\/"(v64"/\"v65))=v64
proof let v65,v64;
(v65"/\"v64)=(v64"/\"v65) by A2,A3,MeetCom;
hence thesis by A55;
end;

A109: for v65,v66,v64 holds
(v64"/\"(v65"\/"(v64"/\"v66)))=(v64"/\"(v65"\/"v66))
proof let v65,v66,v64;
(v66"/\"v64)=(v64"/\"v66) by A2,A3,MeetCom;
hence thesis by A22;
end;

A115: for v1,v65 holds ((v65"/\"v1)"\/"(v1"/\"v65))=(v65"/\"v1)
proof let v1,v65;
((v65"/\"v1)"/\"v65)=(v1"/\"v65) by A86;
hence thesis by A105;
end;

A119: for v64,v66,v65 holds ((v65"\/"v66)"/\"v64)=(v64"/\"(v66"\/"v65))
proof let v64,v66,v65;
(v64"/\"(v65"\/"v66))=((v65"\/"v66)"/\"v64) by A2,A3,MeetCom;
hence thesis by A97;
end;

A123: for v66,v1,v0 holds
((v0"/\"v1)"/\"v66)=(v66"/\"((v1"/\"v0)"\/"(v0"/\"v1)))
proof let v66,v1,v0;
((v0"/\"v1)"\/"(v1"/\"v0))=(v0"/\"v1) by A115;
hence thesis by A119;
end;

A125: for v66,v1,v0 holds ((v0"/\"v1)"/\"v66)=(v66"/\"(v1"/\"v0))
proof let v66,v1,v0;
((v1"/\"v0)"\/"(v0"/\"v1))=(v1"/\"v0) by A115;
hence thesis by A123;
end;

A130: for v66,v64,v0 holds
 (v64"/\"(v66"/\"(v0"\/"v64)))=(v64"/\"((v0"/\"v66)"\/"v66))
proof let v66,v64,v0;
((v0"/\"v66)"\/"(v64"/\"v66))=(v66"/\"(v0"\/"v64)) by A89;
hence thesis by A109;
end;

A132: for v66,v64,v0 holds (v64"/\"(v66"/\"(v0"\/"v64)))=(v64"/\"v66)
proof let v66,v64,v0;
((v0"/\"v66)"\/"v66)=v66 by A57;
hence thesis by A130;
end;

A136: for v65,v66,v64 holds (v64"/\"((v64"\/"v66)"/\"v65))=(v64"/\"v65)
proof let v65,v66,v64;
(v65"/\"(v66"\/"v64))=((v64"\/"v66)"/\"v65) by A119;
hence thesis by A132;
end;

A140: for v65,v64,v66 holds (((v66"\/"v64)"/\"v65)"/\"v64)=(v64"/\"v65)
proof let v65,v64,v66;
(v64"/\"(v65"/\"(v66"\/"v64)))=(((v66"\/"v64)"/\"v65)"/\"v64) by A125;
hence thesis by A132;
end;

A144: for v66,v1,v65 holds ((v65"/\"v1)"/\"(v65"/\"v66))=((v65"/\"v1)"/\"v66)
proof let v66,v1,v65;
((v65"/\"v1)"\/"v65)=v65 by A101;
hence thesis by A136;
end;

A148: for v1,v66,v64 holds ((v64"/\"v66)"/\"(v64"/\"v1))=((v64"/\"v1)"/\"v66)
proof let v1,v66,v64;
(v64"\/"(v64"/\"v1))=v64 by A105;
hence thesis by A140;
end;

A150: for v1,v66,v64 holds ((v64"/\"v66)"/\"v1)=((v64"/\"v1)"/\"v66)
proof let v1,v66,v64;
((v64"/\"v66)"/\"(v64"/\"v1))=((v64"/\"v66)"/\"v1) by A144;
hence thesis by A148;
end;

AA: for v66,v65,v64 holds (v66"/\"(v64"/\"v65))=((v64"/\"v66)"/\"v65)
proof let v66,v65,v64;
((v64"/\"v65)"/\"v66)=(v66"/\"(v64"/\"v65)) by A2,A3,MeetCom;
hence thesis by A150;
end;
let v0,v1,v2;
(v0"/\"(v1"/\"v2))=((v1"/\"v0)"/\"v2) by AA
  .= (v0"/\"v1)"/\"v2 by A2,A3,MeetCom;
hence thesis;
end;

:: Third

theorem ::: trivial
(for v1,v0 holds (v0"/\"(v0"\/"v1))=v0)
implies for v0,v1 holds v0"/\"(v0"\/"v1)=v0;

:: Sixth

theorem MeetAbsor:
L is join-absorbing &
(for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0)))
implies for v1,v0 holds (v0"\/"(v0"/\"v1))=v0
proof
assume A2: L is join-absorbing;

assume A3: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0));

A7: for v65,v66 holds v65=((v66"/\"v65)"\/"(v65"/\"v65))
proof let v65,v66;
(v65"/\"(v65"\/"v66))=v65 by A2;
hence thesis by A3;
end;

A51: for v1,v0 holds ((v0"/\"v1)"\/"v1)=v1
proof let v1,v0;
(v1"/\"v1)=v1 by A2,A3,Lemma1;
hence thesis by A7;
end;

A74: for v64,v65 holds ((v65"/\"v64)"\/"v65)=v65
proof let v64,v65;
(v64"/\"v65)=(v65"/\"v64) by A2,A3,MeetCom;
hence thesis by A51;
end;

let v1,v0;
((v0"/\"v1)"\/"v0)=v0 by A74;
hence thesis by A2,A3,JoinCom;
end;

:: Join-associativity

theorem JoinAssoc:
L is join-absorbing &
(for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0)))
implies for v0,v1,v2 holds (v0"\/"v1)"\/"v2=v0"\/"(v1"\/"v2)
proof
assume A2: L is join-absorbing;
assume A3: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0));

A7: for v65,v66 holds v65=((v66"/\"v65)"\/"(v65"/\"v65))
proof let v65,v66;
(v65"/\"(v65"\/"v66))=v65 by A2;
hence thesis by A3;
end;

A11: for v1,v0 holds ((v0"/\"v1)"/\"v1)=(v0"/\"v1)
proof let v1,v0;
((v0"/\"v1)"\/"(v1"/\"v1))=v1 by A7;
hence thesis by A2;
end;

A14: for v64,v2,v1 holds
 ((v2"/\"(v64"/\"(v1"\/"v2)))"\/"(v1"/\"(v64"/\"(v1"\/"v2))))=
 (v64"/\"(v1"\/"v2))
proof let v64,v2,v1;
((v64"/\"(v1"\/"v2))"/\"(v1"\/"v2))=
((v2"/\"(v64"/\"(v1"\/"v2)))"\/"(v1"/\"(v64"/\"(v1"\/"v2)))) by A3;
hence thesis by A11;
end;

A18: for v65,v64,v0 holds
 ((v0"/\"v64)"\/"(v65"/\"v64))=(v64"/\"(v65"\/"(v0"/\"v64)))
proof let v65,v64,v0;
((v0"/\"v64)"/\"v64)=(v0"/\"v64) by A11;
hence thesis by A3;
end;

A22: for v65,v1,v66 holds
 (v66"\/"(v65"/\"(v66"\/"v1)))=((v66"\/"v1)"/\"(v65"\/"v66))
proof let v65,v1,v66;
(v66"/\"(v66"\/"v1))=v66 by A2;
hence thesis by A3;
end;

A25: for v0,v2,v1 holds ((v2"/\"v0)"/\"(v0"/\"(v1"\/"v2)))=(v2"/\"v0)
proof let v0,v2,v1;
((v2"/\"v0)"\/"(v1"/\"v0))=(v0"/\"(v1"\/"v2)) by A3;
hence thesis by A2;
end;

A29: for v66,v1,v64 holds
 (v64"/\"((v64"\/"v1)"/\"(v66"\/"v64)))=(v64"/\"(v64"\/"v1))
proof let v66,v1,v64;
(v64"/\"(v64"\/"v1))=v64 by A2;
hence thesis by A25;
end;

A31: for v66,v1,v64 holds (v64"/\"((v64"\/"v1)"/\"(v66"\/"v64)))=v64
proof let v66,v1,v64;
(v64"/\"(v64"\/"v1))=v64 by A2;
hence thesis by A29;
end;

A35: for v65,v64,v66 holds (v65"/\"(v66"\/"v64))=(v65"/\"(v66"\/"(v64"/\"v65)))
proof let v65,v64,v66;
((v64"/\"v65)"\/"(v66"/\"v65))=(v65"/\"(v66"\/"v64)) by A3;
hence thesis by A18;
end;

A40: for v64,v0 holds (v64"/\"v64)=(v64"/\"((v0"/\"v64)"\/"v64))
proof let v64,v0;
((v0"/\"v64)"\/"(v64"/\"v64))=v64 by A7;
hence thesis by A35;
end;

A49: for v64,v65 holds ((v64"/\"v64)"\/"((v65"/\"v64)"/\"v64))=(v64"/\"v64)
proof let v64,v65;
(v64"/\"((v65"/\"v64)"\/"v64))=((v64"/\"v64)"\/"((v65"/\"v64)"/\"v64)) by A3;
hence thesis by A40;
end;

A51: for v64,v65 holds ((v64"/\"v64)"\/"(v65"/\"v64))=(v64"/\"v64)
proof let v64,v65;
((v65"/\"v64)"/\"v64)=(v65"/\"v64) by A11;
hence thesis by A49;
end;

A64: for v64,v65 holds (v64"/\"(v65"\/"v64))=(v64"/\"v64)
proof let v64,v65;
((v64"/\"v64)"\/"(v65"/\"v64))=(v64"/\"(v65"\/"v64)) by A3;
hence thesis by A51;
end;

A66: for v64,v65 holds (v64"/\"(v65"\/"v64))=v64
proof let v64,v65;
(v64"/\"v64)=v64 by A2,A3,Lemma1;
hence thesis by A64;
end;

A72: for v0,v1 holds (v0"\/"(v1"/\"v0))=v0
proof let v0,v1;
(v0"\/"(v1"/\"v0))=v0"\/"(v0"/\"v1) by A2,A3,MeetCom .= v0 by A2,A3,MeetAbsor;
hence thesis;
end;

A76: for v1,v0 holds ((v0"/\"v1)"\/"v1)=v1
proof let v1,v0;
(v1"/\"v1)=v1 by A2,A3,Lemma1;
hence thesis by A7;
end;

A91: for v2,v0 holds (v0"/\"(v2"\/"v2))=(v2"/\"v0)
proof let v2,v0;
((v2"/\"v0)"\/"(v2"/\"v0))=(v0"/\"(v2"\/"v2)) by A3;
hence thesis by JoinIdem,A2,A3;
end;

A93: for v2,v0 holds (v0"/\"v2)=(v2"/\"v0)
proof let v2,v0;
(v2"\/"v2)=v2 by JoinIdem,A2,A3;
hence thesis by A91;
end;

A97: for v66,v65,v1 holds
 ((v66"/\"(v1"\/"v65))"\/"v65)=((v1"\/"v65)"/\"(v65"\/"v66))
proof let v66,v65,v1;
(v65"/\"(v1"\/"v65))=v65 by A66;
hence thesis by A3;
end;

A101: for v1,v65 holds ((v65"\/"v1)"\/"v65)=(v65"\/"v1)
proof let v1,v65;
(v65"/\"(v65"\/"v1))=v65 by A2;
hence thesis by A72;
end;

A111: for v64,v65 holds (v64"/\"(v65"/\"v64))=(v65"/\"v64)
proof let v64,v65;
(v64"/\"(v65"/\"v64))=v64"/\"(v64"/\"v65) by A2,A3,MeetCom
  .= v64"/\"v64"/\"v65 by MeetAssoc,A2,A3 .= v64"/\"v65 by A2,A3,Lemma1
  .=v65"/\"v64 by MeetCom,A2,A3;
hence thesis;
end;

A115: for v1,v64 holds
 ((v64"/\"((v64"\/"v1)"/\"(v64"\/"v64)))"\/"v64)=((v64"\/"v1)"/\"(v64"\/"v64))
proof let v1,v64;
(v64"/\"((v64"\/"v1)"/\"(v64"\/"v64)))=v64 by A31;
hence thesis by A14;
end;

A117: for v1,v64 holds
 ((v64"/\"((v64"\/"v1)"/\"v64))"\/"v64)=((v64"\/"v1)"/\"(v64"\/"v64))
proof let v1,v64;
(v64"\/"v64)=v64 by JoinIdem,A2,A3;
hence thesis by A115;
end;

A119: for v1,v64 holds
  (((v64"\/"v1)"/\"v64)"\/"v64)=((v64"\/"v1)"/\"(v64"\/"v64))
proof let v1,v64;
(v64"/\"((v64"\/"v1)"/\"v64))=((v64"\/"v1)"/\"v64) by A111;
hence thesis by A117;
end;

A121: for v1,v64 holds v64=((v64"\/"v1)"/\"(v64"\/"v64))
proof let v1,v64;
(((v64"\/"v1)"/\"v64)"\/"v64)=v64 by A76;
hence thesis by A119;
end;

A123: for v1,v64 holds v64=((v64"\/"v1)"/\"v64)
proof let v1,v64;
(v64"\/"v64)=v64 by JoinIdem,A2,A3;
hence thesis by A121;
end;

A134: for v65,v1,v64 holds (v64"/\"(v65"\/"v64))=(v64"/\"(v65"\/"(v64"\/"v1)))
proof let v65,v1,v64;
((v64"\/"v1)"/\"v64)=v64 by A123;
hence thesis by A35;
end;

A136: for v65,v1,v64 holds v64=(v64"/\"(v65"\/"(v64"\/"v1)))
proof let v65,v1,v64;
(v64"/\"(v65"\/"v64))=v64 by A66;
hence thesis by A134;
end;

A141: for v65,v66,v64 holds
 (v64"\/"((v64"\/"v66)"/\"v65))=((v64"\/"v66)"/\"(v65"\/"v64))
proof let v65,v66,v64;
(v65"/\"(v64"\/"v66))=((v64"\/"v66)"/\"v65) by A93;
hence thesis by A22;
end;

A150: for v1,v66,v64 holds (v64"/\"((v64"\/"v66)"\/"v1))=v64
proof let v1,v66,v64;
(((v64"\/"v66)"\/"v1)"\/"(v64"\/"v66))=((v64"\/"v66)"\/"v1) by A101;
hence thesis by A136;
end;

A160: for v66,v1,v64 holds (v64"\/"v66)=(((v64"\/"v1)"\/"v66)"/\"(v66"\/"v64))
proof let v66,v1,v64;
(v64"/\"((v64"\/"v1)"\/"v66))=v64 by A150;
hence thesis by A97;
end;

A176: for v64,v66,v65 holds ((v65"\/"v66)"\/"v64)=(v64"\/"(v66"\/"v65))
proof let v64,v66,v65;
(v64"\/"(v65"\/"v66))=((v65"\/"v66)"\/"v64) by A2,A3,JoinCom;
hence thesis by A2,A3,JoinCom;
end;

A180: for v66,v65,v64 holds
((v66"\/"v64)"/\"((v64"\/"v65)"\/"v66))=(v64"\/"v66)
proof let v66,v65,v64;
(((v64"\/"v65)"\/"v66)"/\"(v66"\/"v64))=
((v66"\/"v64)"/\"((v64"\/"v65)"\/"v66)) by A93;
hence thesis by A160;
end;

A184: for v65,v1,v0 holds
 ((v0"\/"v1)"\/"(v0"\/"v65))=
 (((v0"\/"v1)"\/"v65)"/\"((v65"\/"v0)"\/"(v0"\/"v1)))
proof let v65,v1,v0;
(((v0"\/"v1)"\/"v65)"/\"(v65"\/"v0))=(v0"\/"v65) by A160;
hence thesis by A141;
end;

A186: for v65,v1,v0 holds ((v0"\/"v1)"\/"(v0"\/"v65))=(v65"\/"(v0"\/"v1))
proof let v65,v1,v0;
(((v0"\/"v1)"\/"v65)"/\"((v65"\/"v0)"\/"(v0"\/"v1)))=
(v65"\/"(v0"\/"v1)) by A180;
hence thesis by A184;
end;

A190: for v65,v66,v64 holds
((v64"\/"v66)"\/"(v65"\/"v64))=(v66"\/"(v64"\/"v65))
proof let v65,v66,v64;
((v64"\/"v65)"\/"(v64"\/"v66))=((v64"\/"v66)"\/"(v65"\/"v64)) by A176;
hence thesis by A186;
end;

A194: for v66,v65,v64 holds
((v64"\/"v65)"\/"(v66"\/"v64))=(v66"\/"(v64"\/"v65))
proof let v66,v65,v64;
((v64"\/"v65)"\/"(v64"\/"v66))=
((v64"\/"v65)"\/"(v66"\/"v64)) by A2,A3,JoinCom;
hence thesis by A186;
end;

A196: for v65,v66,v64 holds (v65"\/"(v64"\/"v66))=(v66"\/"(v64"\/"v65))
proof let v65,v66,v64;
((v64"\/"v65)"\/"(v66"\/"v64))=(v65"\/"(v64"\/"v66)) by A190;
hence thesis by A194;
end;

let v0,v1,v2;
v0"\/"(v1"\/"v2)=v2"\/"(v1"\/"v0) by A196 .=(v1"\/"v0)"\/"v2 by A2,A3,JoinCom
   .= (v0"\/"v1)"\/"v2 by A2,A3,JoinCom;
hence thesis;
end;

:: Seventh file

theorem Seventh:
L is join-absorbing &
(for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0)))
implies for v0,v1,v2 holds v0"/\"(v1"\/"v2)=(v0"/\"v1)"\/"(v0"/\"v2)
proof
assume A3: L is join-absorbing;

assume A4: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0));

A72: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v1"/\"v0)"\/"(v2"/\"v0))
proof let v0,v2,v1;
((v2"/\"v0)"\/"(v1"/\"v0))=(v0"/\"(v1"\/"v2)) by A4;
hence thesis by A3,A4,JoinCom;
end;

A79: for v66,v64,v65 holds ((v65"/\"v64)"\/"(v66"/\"v65))=(v65"/\"(v64"\/"v66))
proof let v66,v64,v65;
(v64"/\"v65)=(v65"/\"v64) by A3,A4,MeetCom;
hence thesis by A72;
end;

let v0,v1,v2;
v0"/\"(v1"\/"v2)=(v0"/\"v1)"\/"(v2"/\"v0) by A79
.=(v0"/\"v1)"\/"(v0"/\"v2) by A3,A4,MeetCom;
hence thesis;
end;

:: Eighth File

theorem
L is join-absorbing &
(for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0))) implies
for v0,v1,v2 holds (v0"\/"(v1"/\"v2))=((v0"\/"v1)"/\"(v0"\/"v2))

proof
assume A2: L is join-absorbing;

assume A3: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0));

A7: for v65,v66 holds v65=((v66"/\"v65)"\/"(v65"/\"v65))
proof let v65,v66;
(v65"/\"(v65"\/"v66))=v65 by A2;
hence thesis by A3;
end;

A12: for v1,v64,v2 holds
 (((v2"/\"v64)"\/"(v1"/\"v64))"\/"((v1"\/"v2)"/\"(v1"\/"v2)))=(v1"\/"v2)
proof let v1,v64,v2;
(v64"/\"(v1"\/"v2))=((v2"/\"v64)"\/"(v1"/\"v64)) by A3;
hence thesis by A7;
end;

A15: for v1,v0 holds ((v0"/\"v1)"/\"v1)=(v0"/\"v1)
proof let v1,v0;
((v0"/\"v1)"/\"v1)=v0"/\"(v1"/\"v1) by A2,A3,MeetAssoc
  .= v0"/\"v1 by A2,A3,Lemma1;
hence thesis;
end;

A22: for v65,v64,v0 holds
 ((v0"/\"v64)"\/"(v65"/\"v64))=(v64"/\"(v65"\/"(v0"/\"v64)))
proof let v65,v64,v0;
((v0"/\"v64)"/\"v64)=(v0"/\"v64) by A15;
hence thesis by A3;
end;

A26: for v66,v1,v65 holds
 ((v66"/\"(v65"\/"v1))"\/"v65)=((v65"\/"v1)"/\"(v65"\/"v66))
proof let v66,v1,v65;
(v65"/\"(v65"\/"v1))=v65 by A2;
hence thesis by A3;
end;

A29: for v0,v2,v1 holds ((v2"/\"v0)"/\"(v0"/\"(v1"\/"v2)))=(v2"/\"v0)
proof let v0,v2,v1;
  ((v2"/\"v0)"\/"(v1"/\"v0))=(v0"/\"(v1"\/"v2)) by A3;
  hence thesis by A2;
end;

A39: for v65,v64,v66 holds (v65"/\"(v66"\/"v64))=(v65"/\"(v66"\/"(v64"/\"v65)))
proof let v65,v64,v66;
((v64"/\"v65)"\/"(v66"/\"v65))=(v65"/\"(v66"\/"v64)) by A3;
hence thesis by A22;
end;

A44: for v0,v65,v64 holds
 (((v64"/\"v65)"\/"(v0"/\"v65))"\/"(((v0"/\"v65)"\/"v64)"/\"
 ((v0"/\"v65)"\/"v64)))=(v0"/\"v65)"\/"v64
proof let v0,v65,v64;
((v0"/\"v65)"/\"v65)=(v0"/\"v65) by A15;
hence thesis by A12;
end;

A53: for v66,v1,v65,v2 holds
 ((v66"/\"(v1"\/"(v2"/\"v65)))"\/"(v65"/\"(v1"\/"v2)))=
 ((v1"\/"(v2"/\"v65))"/\"(v65"\/"v66))
proof let v66,v1,v65,v2;
  (v65"/\"(v1"\/"(v2"/\"v65)))=(v65"/\"(v1"\/"v2)) by A39;
  hence thesis by A3;
end;

A89: for v2,v1,v0 holds
 (((v0"/\"v1)"\/"(v2"/\"v1))"\/"((v2"/\"v1)"\/"v0))=((v2"/\"v1)"\/"v0)
proof let v2,v1,v0;
(((v2"/\"v1)"\/"v0)"/\"((v2"/\"v1)"\/"v0))=((v2"/\"v1)"\/"v0) by A2,A3,Lemma1;
hence thesis by A44;
end;

A94: for v0,v1 holds (v0"\/"(v1"\/"v0))=(v1"\/"v0)
proof let v0,v1;
(v0"\/"(v1"\/"v0))=(v0"\/"(v0"\/"v1)) by JoinCom,A2,A3
.= v0"\/"v0"\/"v1 by JoinAssoc,A2,A3
.= v0"\/"v1 by JoinIdem,A2,A3
.= v1"\/"v0 by JoinCom,A2,A3;
hence thesis;
end;

A121: for v64,v65 holds (v64"/\"(v65"/\"v64))=(v65"/\"v64)
proof let v64,v65;
(v64"/\"(v65"/\"v64))=v64"/\"(v64"/\"v65) by MeetCom,A2,A3
   .= v64"/\"v64"/\"v65 by MeetAssoc,A2,A3
   .= v64"/\"v65 by A2,A3,Lemma1;
hence thesis by A2,A3,MeetCom;
end;

A137: for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v1"/\"v0)"\/"(v2"/\"v0))
proof let v0,v2,v1;
((v2"/\"v0)"\/"(v1"/\"v0))=(v0"/\"(v1"\/"v2)) by A3;
hence thesis by A2,A3,JoinCom;
end;

A140: for v1,v2,v0 holds
 ((v1"/\"(v0"\/"v2))"\/"((v2"/\"v1)"\/"v0))=((v2"/\"v1)"\/"v0)
proof let v1,v2,v0;
((v0"/\"v1)"\/"(v2"/\"v1))=(v1"/\"(v0"\/"v2)) by A137;
hence thesis by A89;
end;

A150: for v1,v65 holds (v65"/\"(v65"/\"v1))=(v65"/\"v1)
proof let v1,v65;
(v65"/\"(v65"/\"v1))=v65"/\"v65"/\"v1 by A2,A3,MeetAssoc
.=(v65"/\"v1) by A2,A3,Lemma1;
hence thesis;
end;

A154: for v64,v2,v65 holds
 ((v64"/\"(v65"\/"v2))"\/"v65)=((v65"\/"(v2"/\"v64))"/\"(v65"\/"v64))
proof let v64,v2,v65;
(v64"/\"(v65"\/"(v2"/\"v64)))=(v64"/\"(v65"\/"v2)) by A39;
hence thesis by A26;
end;

A156: for v64,v2,v65 holds
 ((v65"\/"v2)"/\"(v65"\/"v64))=((v65"\/"(v2"/\"v64))"/\"(v65"\/"v64))
proof let v64,v2,v65;
((v64"/\"(v65"\/"v2))"\/"v65)=((v65"\/"v2)"/\"(v65"\/"v64)) by A26;
hence thesis by A154;
end;

A161: for v66,v64,v1 holds
 ((v1"/\"v64)"/\"((v1"/\"v64)"/\"(v66"\/"v64)))=(v64"/\"(v1"/\"v64))
proof let v66,v64,v1;
(v64"/\"(v1"/\"v64))=(v1"/\"v64) by A121;
hence thesis by A29;
end;

A163: for v66,v64,v1 holds ((v1"/\"v64)"/\"(v66"\/"v64))=(v64"/\"(v1"/\"v64))
proof let v66,v64,v1;
((v1"/\"v64)"/\"((v1"/\"v64)"/\"(v66"\/"v64)))=
((v1"/\"v64)"/\"(v66"\/"v64)) by A150;
hence thesis by A161;
end;

A165: for v66,v64,v1 holds ((v1"/\"v64)"/\"(v66"\/"v64))=(v1"/\"v64)
proof let v66,v64,v1;
(v64"/\"(v1"/\"v64))=(v1"/\"v64) by A121;
hence thesis by A163;
end;

A169: for v65,v66,v0 holds
 ((v0"/\"v66)"\/"v65)=((v65"\/"v66)"/\"(v65"\/"(v0"/\"v66)))
proof let v65,v66,v0;
((v0"/\"v66)"/\"(v65"\/"v66))=(v0"/\"v66) by A165;
hence thesis by A26;
end;

A173: for v64,v65,v67,v66 holds
 ((v67"/\"(v65"\/"v66))"\/"(v64"/\"(v65"\/"(v66"/\"v67))))=
 ((v65"\/"(v66"/\"v67))"/\"(v67"\/"v64))
proof let v64,v65,v67,v66;
((v64"/\"(v65"\/"(v66"/\"v67)))"\/"(v67"/\"(v65"\/"v66)))=
((v67"/\"(v65"\/"v66))"\/"
(v64"/\"(v65"\/"(v66"/\"v67)))) by A2,A3,JoinCom;
hence thesis by A53;
end;

A177: for v64,v66,v65 holds
 ((v64"/\"(v65"\/"v66))"\/"((v65"\/"v64)"/\"(v65"\/"(v66"/\"v64))))=
 ((v66"/\"v64)"\/"v65)
proof let v64,v66,v65;
((v66"/\"v64)"\/"v65)=((v65"\/"v64)"/\"(v65"\/"(v66"/\"v64))) by A169;
hence thesis by A140;
end;

A179: for v65,v64,v66 holds
 ((v65"\/"(v66"/\"v64))"/\"(v64"\/"(v65"\/"v64)))=((v66"/\"v64)"\/"v65)
proof let v65,v64,v66;
((v64"/\"(v65"\/"v66))"\/"((v65"\/"v64)"/\"(v65"\/"(v66"/\"v64))))=((v65"\/"
(v66"/\"v64))"/\"(v64"\/"(v65"\/"v64))) by A173;
hence thesis by A177;
end;

A181: for v65,v64,v66 holds
 ((v65"\/"(v66"/\"v64))"/\"(v65"\/"v64))=((v66"/\"v64)"\/"v65)
proof let v65,v64,v66;
(v64"\/"(v65"\/"v64))=(v65"\/"v64) by A94;
hence thesis by A179;
end;

A183: for v64,v66,v65 holds
((v65"\/"v66)"/\"(v65"\/"v64))=((v66"/\"v64)"\/"v65)
proof let v64,v66,v65;
((v65"\/"(v66"/\"v64))"/\"(v65"\/"v64))=((v65"\/"v66)"/\"(v65"\/"v64)) by A156;
hence thesis by A181;
end;

let v0,v1,v2;
v0"\/"(v1"/\"v2) = ((v1"/\"v2)"\/"v0) by A2,A3,JoinCom
  .=((v0"\/"v1)"/\"(v0"\/"v2)) by A183;
hence thesis;
end;

:: Ordinary Eight Axioms for Distributive Lattices Imply Sholander

 reserve L for distributive join-commutative meet-commutative
   non empty LattStr;
 reserve v0,v1,v2 for Element of L;

theorem LatToSho:
  for v0,v1,v2 holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0)
    by LATTICES:def 11;

theorem Combined:
  for L being non empty LattStr holds
    L is distributive Lattice iff
      L is join-absorbing satisfying_Sholander_1
  proof
    let L be non empty LattStr;
    thus L is distributive Lattice implies
      L is join-absorbing satisfying_Sholander_1 by LatToSho;
    assume
A1: L is join-absorbing satisfying_Sholander_1; then
A2: for v0,v2,v1 being Element of L
      holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0);
    then
A3: L is distributive by Seventh,A1;
A4: L is meet-commutative join-commutative by A2,A1,MeetCom,JoinCom;
A5: L is meet-associative join-associative by A2,A1,MeetAssoc,JoinAssoc;
    for v0,v1 being Element of L holds
      (v0 "/\" v1) "\/" v1 = v1
    proof
      let v0,v1 be Element of L;
      (v0 "/\" v1) "\/" v1 = v1 "\/" (v0 "/\" v1) by A4
         .= v1 "\/" (v1 "/\" v0) by A4
         .= v1 by MeetAbsor,A1,A2;
      hence thesis;
    end; then
    L is meet-absorbing;
    hence thesis by A3,A4,A5,A1;
  end;

registration
  cluster join-absorbing satisfying_Sholander_1 -> distributive Lattice-like
      for non empty LattStr;
  coherence by Combined;
  cluster distributive join-commutative meet-commutative ->
    satisfying_Sholander_1 for non empty LattStr;
  coherence by LatToSho;
end;

begin :: McKenzie axiomatization of lattices

 reserve L for non empty LattStr;
 reserve v103,v3,v102,v101,v100,v2,v1,v0 for Element of L;

definition let L;
  attr L is satisfying_McKenzie_1 means
  for v1,v2,v0 holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0;
  attr L is satisfying_McKenzie_2 means
  for v1,v2,v0 holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0;
  attr L is satisfying_McKenzie_3 means
  for v2,v1,v0 holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1;
  attr L is satisfying_McKenzie_4 means
  for v2,v1,v0 holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1;
end;

theorem MainMcKenzie:
(L is satisfying_McKenzie_1 satisfying_McKenzie_2 &
(for v2,v1,v0 holds ((v0"/\"v1)"\/"(v1"/\"v2))"\/"v1 = v1) &
(for v2,v1,v0 holds ((v0"\/"v1)"/\"(v1"\/"v2))"/\"v1 = v1))
implies
((for v1,v0 holds (v0"/\"(v0"\/"v1))=v0) &
(for v1,v0 holds (v0"\/"(v0"/\"v1))=v0) &
L is join-commutative meet-commutative meet-associative join-associative)
proof
assume A2: L is satisfying_McKenzie_1;
assume A3: L is satisfying_McKenzie_2;
assume A4: for v2,v1,v0 holds (((v0"/\"v1)"\/"(v1"/\"v2))"\/"v1)=v1;
assume A5: for v2,v1,v0 holds (((v0"\/"v1)"/\"(v1"\/"v2))"/\"v1)=v1;
A9: for v100,v101 holds (v100"\/"(v101"/\"v100))=v100
proof
 now let v101,v1,v2,v100;
(v100"/\"(v1"\/"(v100"\/"v2)))=v100 by A3;
hence (v100"\/"(v101"/\"v100))=v100 by A2;
end;
hence thesis;
end;

A13: for v100,v101 holds (v100"/\"(v101"\/"v100))=v100
proof
 now let v101,v1,v2,v100;
(v100"\/"(v1"/\"(v100"/\"v2)))=v100 by A2;
hence (v100"/\"(v101"\/"v100))=v100 by A3;
end;
hence thesis;
end;

A17: for v101,v100 holds ((v100"/\"v101)"\/"v101)=v101
proof
 now let v2,v101,v100;
((v100"/\"v101)"\/"(v101"/\"((v100"/\"v101)"/\"v2)))=(v100"/\"v101) by A2;
hence ((v100"/\"v101)"\/"v101)=v101 by A4;
end;
hence thesis;
end;

A21: for v102,v100 holds (v100"/\"(v100"\/"v102))=v100
proof
 now let v2,v0,v102,v100;
(((v0"/\"(v100"\/"v102))"\/"((v100"\/"v102)"/\"v2))"\/"(v100"\/"v102))
=(v100"\/"v102)
 by A4;
hence (v100"/\"(v100"\/"v102))=v100 by A3;
end;
hence thesis;
end;

A25: for v102,v1,v2,v100 holds
 ((v100"\/"((v1"\/"(v100"\/"v2))"/\"v102))"\/"(v1"\/"(v100"\/"v2)))=
 (v1"\/"(v100"\/"v2))
proof let v102,v1,v2,v100;
(v100"/\"(v1"\/"(v100"\/"v2)))=v100 by A3;
hence thesis by A4;
end;

A33: for v102,v100 holds (v100"\/"(v100"/\"v102))=v100
proof
 now let v2,v0,v102,v100;
(((v0"\/"(v100"/\"v102))"/\"((v100"/\"v102)"\/"v2))"/\"(v100"/\"v102))=
(v100"/\"v102)
 by A5;
hence (v100"\/"(v100"/\"v102))=v100 by A2;
end;
hence thesis;
end;

A37: for v102,v1,v2,v100 holds
 ((v100"/\"((v1"/\"(v100"/\"v2))"\/"v102))"/\"(v1"/\"(v100"/\"v2)))=
 (v1"/\"(v100"/\"v2))
proof let v102,v1,v2,v100;
(v100"\/"(v1"/\"(v100"/\"v2)))=v100 by A2;
hence thesis by A5;
end;

A41: for v101,v100 holds ((v100"\/"v101)"/\"v101)=v101
proof
 now let v2,v101,v100;
((v100"\/"v101)"/\"(v101"\/"((v100"\/"v101)"\/"v2)))=(v100"\/"v101) by A3;
hence ((v100"\/"v101)"/\"v101)=v101 by A5;
end;
hence thesis;
end;

A49: for v102,v100,v1 holds
 ((v100"/\"((v1"/\"v100)"\/"v102))"/\"(v1"/\"v100))=(v1"/\"v100)
proof let v102,v100,v1;
(v100"\/"(v1"/\"v100))=v100 by A9;
hence thesis by A5;
end;

A53: for v102,v100,v1 holds
 ((v100"\/"((v1"\/"v100)"/\"v102))"\/"(v1"\/"v100))=(v1"\/"v100)
proof let v102,v100,v1;
(v100"/\"(v1"\/"v100))=v100 by A13;
hence thesis by A4;
end;

A57: for v1,v2,v100 holds (v100"\/"(v1"\/"(v100"\/"v2)))=(v1"\/"(v100"\/"v2))
proof let v1,v2,v100;
(v100"/\"(v1"\/"(v100"\/"v2)))=v100 by A3;
hence thesis by A17;
end;

A61: for v100,v1 holds (v100"\/"(v1"\/"v100))=(v1"\/"v100)
proof let v100,v1;
(v100"/\"(v1"\/"v100))=v100 by A13;
hence thesis by A17;
end;

A65: for v1,v101 holds ((v101"\/"v1)"\/"v101)=(v101"\/"v1)
proof let v1,v101;
(v101"/\"(v101"\/"v1))=v101 by A21;
hence thesis by A9;
end;

A69: for v1,v100 holds (v100"\/"(v100"\/"v1))=(v100"\/"v1)
proof let v1,v100;
(v100"/\"(v100"\/"v1))=v100 by A21;
hence thesis by A17;
end;

A73: for v1,v101 holds ((v101"/\"v1)"/\"v101)=(v101"/\"v1)
proof let v1,v101;
(v101"\/"(v101"/\"v1))=v101 by A33;
hence thesis by A13;
end;

A77: for v1,v2,v100 holds (v100"/\"(v1"/\"(v100"/\"v2)))=(v1"/\"(v100"/\"v2))
proof let v1,v2,v100;
(v100"\/"(v1"/\"(v100"/\"v2)))=v100 by A2;
hence thesis by A41;
end;

A81: for v100,v1 holds (v100"/\"(v1"/\"v100))=(v1"/\"v100)
proof let v100,v1;
(v100"\/"(v1"/\"v100))=v100 by A9;
hence thesis by A41;
end;

A85: for v1,v2,v101 holds
 ((v1"/\"(v101"/\"v2))"\/"v101)=(v101"\/"(v1"/\"(v101"/\"v2)))
proof let v1,v2,v101;
(v101"\/"(v1"/\"(v101"/\"v2)))=v101 by A2;
hence thesis by A61;
end;

A88: for v0,v2,v1 holds ((v0"/\"(v1"/\"v2))"\/"v1)=v1
proof let v0,v2,v1;
(v1"\/"(v0"/\"(v1"/\"v2)))=v1 by A2;
hence thesis by A85;
end;

A91: for v1,v101 holds ((v101"/\"v1)"\/"v101)=(v101"\/"(v101"/\"v1))
proof let v1,v101;
(v101"\/"(v101"/\"v1))=v101 by A33;
hence thesis by A61;
end;

A94: for v1,v0 holds ((v0"/\"v1)"\/"v0)=v0
proof let v1,v0;
(v0"\/"(v0"/\"v1))=v0 by A33;
hence thesis by A91;
end;

A97: for v1,v102,v100 holds (v100"/\"((v100"\/"v102)"\/"v1))=v100
proof let v1,v102,v100;
(((v100"\/"v102)"\/"v1)"\/"(v100"\/"v102))=((v100"\/"v102)"\/"v1) by A65;
hence thesis by A3;
end;

A101: for v1,v101 holds ((v101"\/"v1)"/\"v101)=v101
proof let v1,v101;
((v101"\/"v1)"\/"v101)=(v101"\/"v1) by A65;
hence thesis by A41;
end;

A105: for v103,v102,v100 holds
 ((v100"\/"v103)"\/"(v103"\/"(v100"\/"v102)))=(v103"\/"(v100"\/"v102))
proof let v103,v102,v100;
((v103"\/"(v100"\/"v102))"/\"v103)=v103 by A101;
hence thesis by A25;
end;

A109: for v101,v100,v1 holds (v100"\/"(v101"/\"(v1"/\"v100)))=v100
proof let v101,v100,v1;
(v100"/\"(v1"/\"v100))=(v1"/\"v100) by A81;
hence thesis by A2;
end;

A113: for v103,v102,v100 holds
 ((v100"/\"v103)"/\"(v103"/\"(v100"/\"v102)))=(v103"/\"(v100"/\"v102))
proof let v103,v102,v100;
((v103"/\"(v100"/\"v102))"\/"v103)=v103 by A94;
hence thesis by A37;
end;

A117: for v1,v102,v101 holds (((v101"/\"v102)"/\"v1)"\/"v101)=v101
proof let v1,v102,v101;
(((v101"/\"v102)"/\"v1)"/\"(v101"/\"v102))=((v101"/\"v102)"/\"v1) by A73;
hence thesis by A88;
end;

A121: for v2,v1,v101 holds
 (((v101"\/"v1)"\/"v2)"/\"v101)=(v101"/\"((v101"\/"v1)"\/"v2))
proof let v2,v1,v101;
(v101"/\"((v101"\/"v1)"\/"v2))=v101 by A97;
hence thesis by A81;
end;

A124: for v2,v1,v0 holds (((v0"\/"v1)"\/"v2)"/\"v0)=v0
proof let v2,v1,v0;
(v0"/\"((v0"\/"v1)"\/"v2))=v0 by A97;
hence thesis by A121;
end;

A127: for v1,v100,v2 holds (v100"/\"(v1"/\"(v2"/\"v100)))=(v1"/\"(v2"/\"v100))
proof let v1,v100,v2;
(v100"\/"(v1"/\"(v2"/\"v100)))=v100 by A109;
hence thesis by A41;
end;

A131: for v0,v102,v101 holds ((v101"/\"v102)"\/"(v0"\/"v101))=(v0"\/"v101)
proof let v0,v102,v101;
((v0"\/"v101)"/\"v101)=v101 by A41;
hence thesis by A117;
end;

A135: for v1,v102,v101 holds ((v101"/\"v102)"\/"(v101"\/"v1))=(v101"\/"v1)
proof let v1,v102,v101;
((v101"\/"v1)"/\"v101)=v101 by A101;
hence thesis by A117;
end;

A139: for v0,v102,v101 holds ((v101"\/"v102)"/\"(v0"/\"v101))=(v0"/\"v101)
proof let v0,v102,v101;
((v0"/\"v101)"\/"v101)=v101 by A17;
hence thesis by A124;
end;

A143: for v102,v100 holds ((v100"/\"v102)"/\"(v102"/\"v100))=(v102"/\"v100)
proof let v102,v100;
((v102"/\"v100)"\/"v102)=v102 by A94;
hence thesis by A49;
end;

A147: for v100,v1,v102 holds
 ((v100"/\"v102)"/\"((v102"/\"v1)"/\"v100))=((v102"/\"v1)"/\"v100)
proof let v100,v1,v102;
(((v102"/\"v1)"/\"v100)"\/"v102)=v102 by A117;
hence thesis by A49;
end;

A151: for v102,v100 holds ((v100"\/"v102)"\/"(v102"\/"v100))=(v102"\/"v100)
proof let v102,v100;
((v102"\/"v100)"/\"v102)=v102 by A101;
hence thesis by A53;
end;

A155: for v100,v101,v2 holds
 ((v100"/\"(v2"\/"v101))"/\"(v101"/\"v100))=(v101"/\"v100)
proof let v100,v101,v2;
((v101"/\"v100)"\/"(v2"\/"v101))=(v2"\/"v101) by A131;
hence thesis by A49;
end;

A159: for v100,v2,v101 holds
 ((v100"/\"(v101"\/"v2))"/\"(v101"/\"v100))=(v101"/\"v100)
proof let v100,v2,v101;
((v101"/\"v100)"\/"(v101"\/"v2))=(v101"\/"v2) by A135;
hence thesis by A49;
end;

A163: for v100,v101,v2 holds
 ((v100"\/"(v2"/\"v101))"\/"(v101"\/"v100))=(v101"\/"v100)
proof let v100,v101,v2;
((v101"\/"v100)"/\"(v2"/\"v101))=(v2"/\"v101) by A139;
hence thesis by A53;
end;

A167: for v1,v0 holds ((v0"/\"v1)"\/"(v1"/\"v0))=(v0"/\"v1)
proof let v1,v0;
((v0"/\"v1)"/\"(v1"/\"v0))=(v1"/\"v0) by A143;
hence thesis by A33;
end;

A170: for v0,v1 holds ((v1"/\"v0)"\/"(v0"/\"v1))=(v0"/\"v1)
proof let v0,v1;
((v0"/\"v1)"/\"(v1"/\"v0))=(v1"/\"v0) by A143;
hence thesis by A94;
end;

A173: for v1,v0 holds (v0"/\"v1)=(v1"/\"v0)
proof let v1,v0;
((v0"/\"v1)"\/"(v1"/\"v0))=(v0"/\"v1) by A167;
hence thesis by A170;
end;

A182: for v1,v0 holds ((v0"\/"v1)"/\"(v1"\/"v0))=(v0"\/"v1)
proof let v1,v0;
((v0"\/"v1)"\/"(v1"\/"v0))=(v1"\/"v0) by A151;
hence thesis by A21;
end;

A185: for v0,v1 holds ((v1"\/"v0)"\/"(v0"\/"v1))=((v0"\/"v1)"\/"(v1"\/"v0))
proof let v0,v1;
((v0"\/"v1)"\/"(v1"\/"v0))=(v1"\/"v0) by A151;
hence thesis by A65;
end;

A188: for v0,v1 holds (v1"\/"v0)=((v1"\/"v0)"\/"(v0"\/"v1))
proof let v0,v1;
((v0"\/"v1)"\/"(v1"\/"v0))=(v1"\/"v0) by A151;
hence thesis by A185;
end;

A191: for v1,v0 holds (v0"\/"v1)=(v1"\/"v0)
proof let v1,v0;
((v0"\/"v1)"\/"(v1"\/"v0))=(v1"\/"v0) by A151;
hence thesis by A188;
end;

A200: for v100,v2,v101 holds
 ((v100"\/"v101)"\/"(v100"\/"(v101"\/"v2)))=(v101"\/"(v100"\/"(v101"\/"v2)))
proof let v100,v2,v101;
(v101"\/"(v100"\/"(v101"\/"v2)))=(v100"\/"(v101"\/"v2)) by A57;
hence thesis by A105;
end;

A203: for v0,v2,v1 holds ((v0"\/"v1)"\/"(v0"\/"(v1"\/"v2)))=(v0"\/"(v1"\/"v2))
proof let v0,v2,v1;
(v1"\/"(v0"\/"(v1"\/"v2)))=(v0"\/"(v1"\/"v2)) by A57;
hence thesis by A200;
end;

A205: for v1,v2,v0 holds ((v0"\/"v1)"\/"((v0"\/"v2)"\/"v1))=(v1"\/"(v0"\/"v2))
proof let v1,v2,v0;
(v1"\/"(v0"\/"v2))=((v0"\/"v2)"\/"v1) by A191;
hence thesis by A105;
end;

A208: for v102,v100,v1 holds
 ((v100"\/"(v102"\/"(v1"/\"v100)))"\/"(v100"\/"v102))=
 ((v102"\/"(v1"/\"v100))"\/"(v100"\/"v102))
proof let v102,v100,v1;
((v102"\/"(v1"/\"v100))"\/"(v100"\/"v102))=(v100"\/"v102) by A163;
hence thesis by A105;
end;

A211: for v1,v0,v2 holds
 ((v0"\/"v1)"\/"(v0"\/"(v1"\/"(v2"/\"v0))))=((v1"\/"(v2"/\"v0))"\/"(v0"\/"v1))
proof let v1,v0,v2;
((v0"\/"(v1"\/"(v2"/\"v0)))"\/"(v0"\/"v1))=
((v0"\/"v1)"\/"(v0"\/"(v1"\/"(v2"/\"v0)))) by A191;
hence thesis by A208;
end;

A213: for v1,v0,v2 holds
 (v0"\/"(v1"\/"(v2"/\"v0)))=((v1"\/"(v2"/\"v0))"\/"(v0"\/"v1))
proof let v1,v0,v2;
((v0"\/"v1)"\/"(v0"\/"(v1"\/"(v2"/\"v0))))=(v0"\/"(v1"\/"(v2"/\"v0))) by A203;
hence thesis by A211;
end;

A215: for v1,v0,v2 holds (v0"\/"(v1"\/"(v2"/\"v0)))=(v0"\/"v1)
proof let v1,v0,v2;
((v1"\/"(v2"/\"v0))"\/"(v0"\/"v1))=(v0"\/"v1) by A163;
hence thesis by A213;
end;

A218: for v101,v102,v1 holds
 ((v1"\/"v102)"\/"(v101"\/"v102))=((v1"\/"v102)"\/"v101)
proof let v101,v102,v1;
(v102"/\"(v1"\/"v102))=v102 by A13;
hence thesis by A215;
end;

A221: for v1,v0,v2 holds (v0"\/"((v2"/\"v0)"\/"v1))=(v0"\/"v1)
proof let v1,v0,v2;
(v1"\/"(v2"/\"v0))=((v2"/\"v0)"\/"v1) by A191;
hence thesis by A215;
end;

A224: for v2,v1,v0 holds ((v0"\/"v1)"\/"(v0"\/"v2))=(v1"\/"(v0"\/"v2))
proof let v2,v1,v0;
((v0"\/"v1)"\/"((v0"\/"v2)"\/"v1))=((v0"\/"v1)"\/"(v0"\/"v2)) by A218;
hence thesis by A205;
end;

A227: for v102,v1,v101 holds
 ((v101"\/"v1)"\/"(v101"\/"v102))=((v101"\/"v1)"\/"v102)
proof let v102,v1,v101;
(v101"/\"(v101"\/"v1))=v101 by A21;
hence thesis by A221;
end;

A230: for v1,v2,v0 holds (v1"\/"(v0"\/"v2))=((v0"\/"v1)"\/"v2)
proof let v1,v2,v0;
((v0"\/"v1)"\/"(v0"\/"v2))=(v1"\/"(v0"\/"v2)) by A224;
hence thesis by A227;
end;

A236: for v102,v1,v0 holds
 ((v1"\/"v0)"\/"((v0"\/"v1)"\/"v102))=((v1"\/"v0)"\/"v102)
proof let v102,v1,v0;
((v0"\/"v1)"/\"(v1"\/"v0))=(v0"\/"v1) by A182;
hence thesis by A221;
end;

A239: for v0,v2,v1 holds ((v0"\/"v1)"\/"(v0"\/"(v1"\/"v2)))=((v0"\/"v1)"\/"v2)
proof let v0,v2,v1;
((v1"\/"v0)"\/"v2)=(v0"\/"(v1"\/"v2)) by A230;
hence thesis by A236;
end;

A241: for v0,v2,v1 holds (v1"\/"(v0"\/"(v0"\/"(v1"\/"v2))))=((v0"\/"v1)"\/"v2)
proof let v0,v2,v1;
((v0"\/"v1)"\/"(v0"\/"(v1"\/"v2)))=(v1"\/"(v0"\/"(v0"\/"(v1"\/"v2)))) by A230;
hence thesis by A239;
end;

A244: for v1,v2,v0 holds (v0"\/"(v1"\/"(v0"\/"v2)))=((v1"\/"v0)"\/"v2)
proof let v1,v2,v0;
(v1"\/"(v1"\/"(v0"\/"v2)))=(v1"\/"(v0"\/"v2)) by A69;
hence thesis by A241;
end;

A246: for v1,v2,v0 holds (v1"\/"(v0"\/"v2))=((v1"\/"v0)"\/"v2)
proof let v1,v2,v0;
(v0"\/"(v1"\/"(v0"\/"v2)))=(v1"\/"(v0"\/"v2)) by A57;
hence thesis by A244;
end;

A257: for v1,v2,v0 holds ((v1"/\"v0)"/\"(v1"/\"(v0"/\"v2)))=(v1"/\"(v0"/\"v2))
proof let v1,v2,v0;
(v0"/\"v1)=(v1"/\"v0) by A173;
hence thesis by A113;
end;

A261: for v102,v100,v1 holds
 ((v100"/\"(v102"/\"(v1"\/"v100)))"/\"(v100"/\"v102))=
 ((v102"/\"(v1"\/"v100))"/\"(v100"/\"v102))
proof let v102,v100,v1;
((v102"/\"(v1"\/"v100))"/\"(v100"/\"v102))=(v100"/\"v102) by A155;
hence thesis by A113;
end;

A264: for v1,v0,v2 holds
 ((v0"/\"v1)"/\"(v0"/\"(v1"/\"(v2"\/"v0))))=((v1"/\"(v2"\/"v0))"/\"(v0"/\"v1))
proof let v1,v0,v2;
((v0"/\"(v1"/\"(v2"\/"v0)))"/\"(v0"/\"v1))=
((v0"/\"v1)"/\"(v0"/\"(v1"/\"(v2"\/"v0)))) by A173;
hence thesis by A261;
end;

A266: for v1,v0,v2 holds
 (v0"/\"(v1"/\"(v2"\/"v0)))=((v1"/\"(v2"\/"v0))"/\"(v0"/\"v1))
proof let v1,v0,v2;
((v0"/\"v1)"/\"(v0"/\"(v1"/\"(v2"\/"v0))))=(v0"/\"(v1"/\"(v2"\/"v0))) by A257;
hence thesis by A264;
end;

A268: for v1,v0,v2 holds (v0"/\"(v1"/\"(v2"\/"v0)))=(v0"/\"v1)
proof let v1,v0,v2;
((v1"/\"(v2"\/"v0))"/\"(v0"/\"v1))=(v0"/\"v1) by A155;
hence thesis by A266;
end;

A271: for v101,v0,v2,v1 holds
 (((v0"/\"(v1"\/"v2))"/\"v101)"/\"(v101"/\"(v1"/\"v0)))=
 (v101"/\"((v0"/\"(v1"\/"v2))"/\"(v1"/\"v0)))
proof let v101,v0,v2,v1;
((v0"/\"(v1"\/"v2))"/\"(v1"/\"v0))=(v1"/\"v0) by A159;
hence thesis by A113;
end;

A274: for v3,v0,v2,v1 holds
 (((v0"/\"(v1"\/"v2))"/\"v3)"/\"(v3"/\"(v1"/\"v0)))=(v3"/\"(v1"/\"v0))
proof let v3,v0,v2,v1;
((v0"/\"(v1"\/"v2))"/\"(v1"/\"v0))=(v1"/\"v0) by A159;
hence thesis by A271;
end;

A277: for v102,v2,v100 holds
 ((v100"/\"(v102"/\"(v100"\/"v2)))"/\"(v100"/\"v102))=
 ((v102"/\"(v100"\/"v2))"/\"(v100"/\"v102))
proof let v102,v2,v100;
((v102"/\"(v100"\/"v2))"/\"(v100"/\"v102))=(v100"/\"v102) by A159;
hence thesis by A113;
end;

A280: for v1,v2,v0 holds
 ((v0"/\"v1)"/\"(v0"/\"(v1"/\"(v0"\/"v2))))=((v1"/\"(v0"\/"v2))"/\"(v0"/\"v1))
proof let v1,v2,v0;
((v0"/\"(v1"/\"(v0"\/"v2)))"/\"(v0"/\"v1))=
((v0"/\"v1)"/\"(v0"/\"(v1"/\"(v0"\/"v2)))) by A173;
hence thesis by A277;
end;

A282: for v1,v2,v0 holds
 (v0"/\"(v1"/\"(v0"\/"v2)))=((v1"/\"(v0"\/"v2))"/\"(v0"/\"v1))
proof let v1,v2,v0;
((v0"/\"v1)"/\"(v0"/\"(v1"/\"(v0"\/"v2))))=(v0"/\"(v1"/\"(v0"\/"v2))) by A257;
hence thesis by A280;
end;

A284: for v1,v2,v0 holds (v0"/\"(v1"/\"(v0"\/"v2)))=(v0"/\"v1)
proof let v1,v2,v0;
((v1"/\"(v0"\/"v2))"/\"(v0"/\"v1))=(v0"/\"v1) by A159;
hence thesis by A282;
end;

A287: for v101,v1,v102 holds
 ((v102"/\"v1)"/\"(v101"/\"v102))=((v102"/\"v1)"/\"v101)
proof let v101,v1,v102;
(v102"\/"(v102"/\"v1))=v102 by A33;
hence thesis by A268;
end;

A290: for v1,v0,v2 holds (v0"/\"((v2"\/"v0)"/\"v1))=(v0"/\"v1)
proof let v1,v0,v2;
(v1"/\"(v2"\/"v0))=((v2"\/"v0)"/\"v1) by A173;
hence thesis by A268;
end;

A293: for v2,v1,v0 holds ((v0"/\"v1)"/\"(v1"/\"v2))=((v1"/\"v2)"/\"v0)
proof let v2,v1,v0;
((v0"/\"v1)"/\"((v1"/\"v2)"/\"v0))=((v0"/\"v1)"/\"(v1"/\"v2)) by A287;
hence thesis by A147;
end;

A295: for v1,v2,v0 holds (v0"/\"((v0"\/"v2)"/\"v1))=(v0"/\"v1)
proof let v1,v2,v0;
(v1"/\"(v0"\/"v2))=((v0"\/"v2)"/\"v1) by A173;
hence thesis by A284;
end;

A299: for v102,v101,v1 holds
 ((v1"/\"v101)"/\"(v101"/\"v102))=((v1"/\"v101)"/\"v102)
proof let v102,v101,v1;
(v101"\/"(v1"/\"v101))=v101 by A9;
hence thesis by A290;
end;

A303: for v102,v1,v101 holds
 ((v101"/\"v1)"/\"(v101"/\"v102))=((v101"/\"v1)"/\"v102)
proof let v102,v1,v101;
(v101"\/"(v101"/\"v1))=v101 by A33;
hence thesis by A290;
end;

A307: for v101,v2,v100,v1 holds
 ((v100"/\"v101)"/\"(v101"/\"(v100"/\"v2)))=
 (v101"/\"(v100"/\"((v1"\/"v100)"/\"v2)))
proof let v101,v2,v100,v1;
(v100"/\"((v1"\/"v100)"/\"v2))=(v100"/\"v2) by A290;
hence thesis by A113;
end;

A310: for v1,v2,v0,v3 holds
 ((v0"/\"v1)"/\"(v0"/\"v2))=(v1"/\"(v0"/\"((v3"\/"v0)"/\"v2)))
proof let v1,v2,v0,v3;
((v0"/\"v1)"/\"(v1"/\"(v0"/\"v2)))=((v0"/\"v1)"/\"(v0"/\"v2)) by A299;
hence thesis by A307;
end;

A312: for v1,v2,v0,v3 holds
((v0"/\"v1)"/\"v2)=(v1"/\"(v0"/\"((v3"\/"v0)"/\"v2)))
proof let v1,v2,v0,v3;
((v0"/\"v1)"/\"(v0"/\"v2))=((v0"/\"v1)"/\"v2) by A303;
hence thesis by A310;
end;

A314: for v2,v1,v0 holds ((v0"/\"v1)"/\"v2)=(v1"/\"(v0"/\"v2))
proof
 now let v1,v2,v0,v3;
(v0"/\"((v3"\/"v0)"/\"v2))=(v0"/\"v2) by A290;
hence ((v0"/\"v1)"/\"v2)=(v1"/\"(v0"/\"v2)) by A312;
end;
hence thesis;
end;

A316: for v0,v2,v1 holds (v1"/\"(v0"/\"(v1"/\"v2)))=((v1"/\"v2)"/\"v0)
proof let v0,v2,v1;
((v0"/\"v1)"/\"(v1"/\"v2))=(v1"/\"(v0"/\"(v1"/\"v2))) by A314;
hence thesis by A293;
end;

A319: for v1,v2,v0 holds (v1"/\"(v0"/\"v2))=((v0"/\"v2)"/\"v1)
proof let v1,v2,v0;
(v0"/\"(v1"/\"(v0"/\"v2)))=(v1"/\"(v0"/\"v2)) by A77;
hence thesis by A316;
end;

A322: for v0,v2,v1 holds (v0"/\"(v1"/\"v2))=(v2"/\"(v1"/\"v0))
proof let v0,v2,v1;
((v1"/\"v2)"/\"v0)=(v2"/\"(v1"/\"v0)) by A314;
hence thesis by A319;
end;

A324: for v0,v3,v2,v1 holds
 (((v1"\/"v2)"/\"(v0"/\"v3))"/\"(v3"/\"(v1"/\"v0)))=(v3"/\"(v1"/\"v0))
proof let v0,v3,v2,v1;
((v0"/\"(v1"\/"v2))"/\"v3)=((v1"\/"v2)"/\"(v0"/\"v3)) by A314;
hence thesis by A274;
end;

A327: for v2,v3,v1,v0 holds
 ((v0"/\"v2)"/\"(v3"/\"((v0"\/"v1)"/\"(v2"/\"v3))))=(v3"/\"(v0"/\"v2))
proof let v2,v3,v1,v0;
(((v0"\/"v1)"/\"(v2"/\"v3))"/\"(v3"/\"(v0"/\"v2)))=
((v0"/\"v2)"/\"(v3"/\"((v0"\/"v1)"/\"(v2"/\"v3)))) by A322;
hence thesis by A324;
end;

A330: for v1,v2,v3,v0 holds
 ((v0"/\"v1)"/\"((v0"\/"v3)"/\"(v1"/\"v2)))=(v2"/\"(v0"/\"v1))
proof let v1,v2,v3,v0;
(v2"/\"((v0"\/"v3)"/\"(v1"/\"v2)))=((v0"\/"v3)"/\"(v1"/\"v2)) by A127;
hence thesis by A327;
end;

A333: for v1,v3,v2,v0 holds
 (v1"/\"(v0"/\"((v0"\/"v2)"/\"(v1"/\"v3))))=(v3"/\"(v0"/\"v1))
proof let v1,v3,v2,v0;
((v0"/\"v1)"/\"((v0"\/"v2)"/\"(v1"/\"v3)))=
(v1"/\"(v0"/\"((v0"\/"v2)"/\"(v1"/\"v3)))) by A314;
hence thesis by A330;
end;

A336: for v1,v3,v0 holds (v0"/\"(v1"/\"(v0"/\"v3)))=(v3"/\"(v1"/\"v0))
proof
 now let v0,v3,v2,v1;
(v1"/\"((v1"\/"v2)"/\"(v0"/\"v3)))=(v1"/\"(v0"/\"v3)) by A295;
hence (v0"/\"(v1"/\"(v0"/\"v3)))=(v3"/\"(v1"/\"v0)) by A333;
end;
hence thesis;
end;

A339: for v1,v2,v0 holds (v1"/\"(v0"/\"v2))=(v2"/\"(v1"/\"v0))
proof let v1,v2,v0;
(v0"/\"(v1"/\"(v0"/\"v2)))=(v1"/\"(v0"/\"v2)) by A77;
hence thesis by A336;
end;

for v0,v2,v1 holds (v0"/\"(v1"/\"v2))=((v0"/\"v1)"/\"v2)
proof
let v0,v2,v1;
(v0"/\"(v1"/\"v2))=(v2"/\"(v0"/\"v1)) by A339 .= ((v0"/\"v1)"/\"v2) by A173;
hence thesis;
end;

hence thesis by A173,A191,A21,A33,A246;
end;

theorem AuxiliaryMcKenzie:
L is join-commutative join-associative meet-commutative meet-associative &
(for v1,v0 holds (v0"/\"(v0"\/"v1))=v0) &
(for v1,v0 holds (v0"\/"(v0"/\"v1))=v0)
implies
(for v1,v2,v0 holds (v0"\/"(v1"/\"(v0"/\"v2)))=v0) &
(for v1,v2,v0 holds (v0"/\"(v1"\/"(v0"\/"v2)))=v0) &
(for v2,v1,v0 holds (((v0"/\"v1)"\/"(v1"/\"v2))"\/"v1)=v1) &
(for v2,v1,v0 holds (((v0"\/"v1)"/\"(v1"\/"v2))"/\"v1)=v1)
proof
assume A2: L is join-commutative;
assume A3: L is join-associative;
assume A4: L is meet-commutative;
assume A5: L is meet-associative;
assume A6: for v1,v0 holds (v0"/\"(v0"\/"v1))=v0;
assume A7: for v1,v0 holds (v0"\/"(v0"/\"v1))=v0;
thus for v1,v2,v0 holds (v0"\/"(v1"/\"(v0"/\"v2)))=v0
proof
  let v1,v2,v0;
  (v0"\/"(v1"/\"(v0"/\"v2)))=(v0"\/"((v1"/\"v0)"/\"v2)) by A5
    .=(v0"\/"((v0"/\"v1)"/\"v2)) by A4
    .=(v0"\/"(v0"/\"(v1"/\"v2))) by A5
    .= v0 by A7;
  hence thesis;
end;

thus for v1,v2,v0 holds (v0"/\"(v1"\/"(v0"\/"v2)))=v0
proof
  let v1,v2,v0;
  (v0"/\"(v1"\/"(v0"\/"v2)))=(v0"/\"((v1"\/"v0)"\/"v2)) by A3
    .=(v0"/\"((v0"\/"v1)"\/"v2)) by A2
    .=(v0"/\"(v0"\/"(v1"\/"v2))) by A3
    .= v0 by A6;
  hence thesis;
end;

thus for v2,v1,v0 holds (((v0"/\"v1)"\/"(v1"/\"v2))"\/"v1)=v1
proof
let v2,v1,v0;
(((v0"/\"v1)"\/"(v1"/\"v2))"\/"v1)=(v0"/\"v1)"\/"((v1"/\"v2)"\/"v1) by A3
  .= (v0"/\"v1)"\/"(v1"\/"(v1"/\"v2)) by A2
  .= (v0"/\"v1)"\/"v1 by A7
  .= v1"\/"(v0"/\"v1) by A2
  .= v1"\/"(v1"/\"v0) by A4
  .= v1 by A7;
hence thesis;
end;

let v2,v1,v0;
(((v0"\/"v1)"/\"(v1"\/"v2))"/\"v1)=(v0"\/"v1)"/\"((v1"\/"v2)"/\"v1) by A5
  .= (v0"\/"v1)"/\"(v1"/\"(v1"\/"v2)) by A4
  .= (v0"\/"v1)"/\"v1 by A6
  .= v1"/\"(v0"\/"v1) by A4
  .= v1"/\"(v1"\/"v0) by A2
  .= v1 by A6;
hence thesis;
end;

definition let L be non empty LattStr;
  attr L is satisfying_4_McKenzie_axioms means
    L is satisfying_McKenzie_1 &
    L is satisfying_McKenzie_2 &
    L is satisfying_McKenzie_3 &
    L is satisfying_McKenzie_4;
end;

registration
  cluster satisfying_4_McKenzie_axioms ->
    satisfying_McKenzie_1 satisfying_McKenzie_2 satisfying_McKenzie_3
      satisfying_McKenzie_4 for non empty LattStr;
  coherence;
  cluster satisfying_McKenzie_1 satisfying_McKenzie_2 satisfying_McKenzie_3
      satisfying_McKenzie_4 -> satisfying_4_McKenzie_axioms
         for non empty LattStr;
  coherence;
end;

theorem CombinedMcKenzie:
  L is Lattice iff
    L is satisfying_4_McKenzie_axioms
  proof
    thus L is Lattice implies
      L is satisfying_4_McKenzie_axioms
    proof
      assume A1: L is Lattice;
C1:   for v1,v0 holds (v0"/\"(v0"\/"v1))=v0 by A1,LATTICES:def 9;
      for v1,v0 holds v0"\/"(v0"/\"v1)=v0
      proof
        let v1,v0;
A2:     L is join-commutative meet-commutative meet-absorbing by A1; then
        v0"\/"(v0"/\"v1) = (v0"/\"v1)"\/"v0
            .=(v1"/\"v0)"\/"v0 by A2
            .=v0 by A2;
        hence thesis;
      end; then
      L is satisfying_McKenzie_1 &
      L is satisfying_McKenzie_2 &
      L is satisfying_McKenzie_3 &
      L is satisfying_McKenzie_4 by AuxiliaryMcKenzie,A1,C1;
      hence thesis;
    end;
    assume L is satisfying_4_McKenzie_axioms; then
b1: L is satisfying_McKenzie_1 &
    L is satisfying_McKenzie_2 &
    L is satisfying_McKenzie_3 &
    L is satisfying_McKenzie_4; then
B1: (for v1,v0 being Element of L holds v0"/\"(v0"\/"v1)=v0) &
    (for v1,v0 being Element of L holds (v0"\/"(v0"/\"v1))=v0) &
    L is join-commutative meet-commutative meet-associative join-associative
      by MainMcKenzie;
B2: for v0,v1 being Element of L holds (v1 "/\" v0) "\/" v0 = v0
    proof
      let v0,v1;
      (v1 "/\" v0) "\/" v0 = v0 "\/" (v1 "/\" v0) by B1
          .= v0 "\/" (v0 "/\" v1) by B1
          .= v0 by b1,MainMcKenzie;
      hence thesis;
    end;
    L is meet-absorbing join-absorbing by b1,B2,MainMcKenzie;
    hence thesis by B1;
  end;

registration
  cluster Lattice-like -> satisfying_4_McKenzie_axioms
    for non empty LattStr;
  coherence by CombinedMcKenzie;
  cluster satisfying_4_McKenzie_axioms -> Lattice-like
    for non empty LattStr;
  coherence by CombinedMcKenzie;
end;