:: On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander :: by Adam Grabowski and Damian Sawicki :: :: Received June 29, 2018 :: Copyright (c) 2018-2019 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 RELSET_1, STRUCT_0, LATTICES, LATTICE2; requirements SUBSET, NUMERALS; definitions 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; reserve L for non empty LattStr; 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;