:: On the Two Short Axiomatizations of Ortholattices :: by Wioletta Truszkowska and Adam Grabowski :: :: Received June 28, 2003 :: Copyright (c) 2003-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, ROBBINS1, SUBSET_1, ARYTM_3, LATTICES, ROBBINS2; notations STRUCT_0, LATTICES, ROBBINS1; constructors ROBBINS1; registrations LATTICES, ROBBINS1, STRUCT_0; theorems ROBBINS1, LATTICES, STRUCT_0; begin :: One Axiom for Boolean Algebra definition let L be non empty ComplLLattStr; attr L is satisfying_DN_1 means :Def1: for x, y, z, u being Element of L holds (((x + y)` + z)` + (x + (z` + (z + u)`)`)`)` = z; end; registration cluster TrivComplLat -> satisfying_DN_1; coherence by STRUCT_0:def 10; cluster TrivOrtLat -> satisfying_DN_1; coherence by STRUCT_0:def 10; end; registration cluster join-commutative join-associative satisfying_DN_1 for non empty ComplLLattStr; existence proof take TrivComplLat; thus thesis; end; end; reserve L for satisfying_DN_1 non empty ComplLLattStr; reserve x, y, z for Element of L; theorem Th1: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u, v being Element of L holds ((x + y)` + (((z + u)` + x)` + (y` + (y + v)`)`)`)` = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z, u, v be Element of L; set X = ((z + u)` + x)`, Y = (z + (x` + (x + u)`)`)`; set Z = y, U = v; (((X + Y)` + Z)` + (X + (Z` + (Z + U)`)`)`)` = Z by Def1; hence thesis by Def1; end; theorem Th2: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u being Element of L holds ((x + y)` + ((z + x)` + (y` + (y + u)`)`)`)` = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z, u be Element of L; set v = the Element of L; ((x + z)` + (((y + u)` + x)` + (z` + (z + v)`)`)`)` = z by Th1; hence thesis by Th1; end; theorem Th3: for L being satisfying_DN_1 non empty ComplLLattStr, x being Element of L holds ((x + x`)` + x)` = x` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x be Element of L; set y = the Element of L; set V = (x + y)`; ((x + x`)` + (((x`` + y)` + x)` + (x`` + (x` + V)`)`)`)` = x` by Th1; hence thesis by Def1; end; theorem Th4: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u being Element of L holds ((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + u)`)` )`)` = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z, u be Element of L; ((y + y`)` + y)` = y` by Th3; hence thesis by Th2; end; theorem Th5: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((x + y)` + ((z + x)` + y)`)` = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set u = the Element of L; set U = (y` + (y + u)`)`; ((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + U)`)`)`)` = y by Th4; hence thesis by Def1; end; theorem Th6: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y)` + (x` + y)`)` = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set Z = (x + x`)`; ((x + y)` + ((Z + x)` + y)`)` = y by Th5; hence thesis by Th3; end; theorem Th7: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (((x + y)` + x)` + (x + y)`)` = x proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set X = (x + y)`; ((X + x)` + ((x + X)` + (((x + x`)` + x)` + (x + y)`)`)`)` = x by Th4; hence thesis by Th5; end; theorem Th8: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + ((x + y)` + x)`)` = (x + y)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set X = (x + y)`, Y = x; (((X + Y)` + X)` + (X + Y)`)` = X by Th7; hence thesis by Th7; end; theorem Th9: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (((x + y)` + z)` + (x + z)`)` = z proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set X = (x + y)`, Y = z, Z = ((x + y)` + x)`; ((X + Y)` + ((Z + X)` + Y)`)` = Y by Th5; hence thesis by Th7; end; theorem Th10: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x + ((y + z)` + (y + x)`)`)` = (y + x)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set Z = (y + x)`, X = (y + z)`, Y = x; (((X + Y)` + Z)` + (X + Z)`)` = Z by Th9; hence thesis by Th9; end; theorem Th11: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((((x + y)` + z)` + (x` + y)`)` + y)` = (x` + y)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set X = (x + y)`, Z = (x` + y)`, Y = z; (((X + Y)` + Z)` + (X + Z)`)` = Z by Th9; hence thesis by Th6; end; theorem Th12: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x + ((y + z)` + (z + x)`)`)` = (z + x)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set Y = z, Z = ((y + x)` + (y + z)`)`; (x + ((Y + Z)` + (Y + x)`)`)` = (Y + x)` by Th10; hence thesis by Th10; end; theorem Th13: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u being Element of L holds ((x + y)` + ((z + x)` + (y` + (u + y)`)`)`)` = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z, u be Element of L; set U = ((u + z)` + (u + y)`)`; ((x + y)` + ((z + x)` + (y` + (y + U)`)`)`)` = y by Th2; hence thesis by Th10; end; theorem Th14: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y)` = (y + x)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set Z = y, X = x, Y = (y + x)`; ((Y + Z)` + (Z + X)`)` = y by Th7; hence thesis by Th12; end; theorem Th15: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (((x + y)` + (y + z)`)` + z)` = (y + z)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set Y = ((x + y)` + (y + z)`)`; (z + Y)` = (Y + z)` by Th14; hence thesis by Th12; end; theorem Th16: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((x + ((x + y)` + z)`)` + z)` = ((x + y)` + z)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set X = ((x + y)` + x)`, Y = (x + y)`; (X + Y)` = x by Th7; hence thesis by Th15; end; theorem Th17: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (((x + y)` + x)` + y)` = (y + y)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set X = (x + y)`; (X + ((X + x)` + y)`)` = y by Th5; hence thesis by Th16; end; theorem Th18: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x` + (y + x)`)` = x proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set X = (y + x)`; (X + ((x` + y)` + (x` + X)`)`)` = x by Th13; hence thesis by Th10; end; theorem Th19: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y)` + y`)` = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; (y` + (x + y)`)` = y by Th18; hence thesis by Th14; end; theorem Th20: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + (y + x`)`)` = x` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set Z = x`, X = y, Y = x; (((X + Y)` + Z)` + (X + Z)`)` = Z by Th9; hence thesis by Th19; end; theorem Th21: for L being satisfying_DN_1 non empty ComplLLattStr, x being Element of L holds (x + x)` = x` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x be Element of L; set y = the Element of L; set Y = (y + x)`; (x + (Y + x`)`)` = x` by Th20; hence thesis by Th19; end; theorem Th22: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (((x + y)` + x)` + y)` = y` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; y` = (y + y)` by Th21 .= (((x + y)` + x)` + y)` by Th17; hence thesis; end; theorem Th23: for L being satisfying_DN_1 non empty ComplLLattStr, x being Element of L holds x`` = x proof let L be satisfying_DN_1 non empty ComplLLattStr; let x be Element of L; x`` = (((x + x`)` + x)` + x`)` by Th22 .= x by Th19; hence thesis; end; theorem Th24: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y)` + x)`+ y = y`` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; (((x + y)` + x)` + y)`` = y`` by Th22; hence thesis by Th23; end; theorem Th25: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y)`` = y + x proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; (x + y)`` = (y + x)`` by Th14 .= y + x by Th23; hence thesis; end; theorem Th26: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + ((y + z)` + (y + x)`)` = (y + x )`` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; (x + ((y + z)` + (y + x)`)`)`` = (y + x)`` by Th10; hence thesis by Th23; end; theorem Th27: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds x + y = y + x proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; x + y = (x + y)`` by Th23 .= y + x by Th25; hence thesis; end; Lm1: for L being satisfying_DN_1 non empty ComplLLattStr holds L is join-commutative proof let L; for x, y holds x + y = y + x by Th27; hence thesis by LATTICES:def 4; end; registration cluster satisfying_DN_1 -> join-commutative for non empty ComplLLattStr; coherence by Lm1; end; theorem Th28: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y)` + x)` + y = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; ((x + y)` + x)` + y = y`` by Th24; hence thesis by Th23; end; theorem for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y)` + y)`+ x = x by Th28; theorem for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds x + ((y + x)` + y)` = x by Th28; theorem Th31: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y`)` + (y` + y)` = (x + y`)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set X = (x + y`)`; X + ((y + X)` + y)` = X by Th28; hence thesis by Th20; end; theorem Th32: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y)` + (y + y`)` = (x + y)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set X = (x + y)`, Y = y`; X + ((Y + X)` + Y)` = X by Th28; hence thesis by Th18; end; theorem for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y)` + (y` + y)` = (x + y)` by Th32; theorem Th34: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y`)`` + y)` = (y` + y)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set Y = y`, Z = y; (((x + Y)` + (Y + Z)`)` + Z)` = (Y + Z)` by Th15; hence thesis by Th31; end; theorem Th35: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds ((x + y`) + y)` = (y` + y)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; ((x + y`)`` + y)` = (y` + y)` by Th34; hence thesis by Th23; end; theorem Th36: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((((x + y`) + z)` + y)` + (y` + y)`)` = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; ((x + y`) + y)` = (y` + y)` by Th35; hence thesis by Th9; end; theorem Th37: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + ((y + z)` + (y + x)`)` = y + x proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; x + ((y + z)` + (y + x)`)` = (y + x )`` by Th26; hence thesis by Th23; end; theorem Th38: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + (y + ((z + y)` + x)`)` = (z + y)` + x proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set Y = (z + y)`, Z = y`; x + ((Y + Z)` + (Y + x)`)` = Y + x by Th37; hence thesis by Th19; end; theorem for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + ((y + x)` + (y + z)`)` = y + x by Th37; theorem Th40: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((x + y)` + ((x + y)` + (x + z)`)`)` + y = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set Y = ((x + y)` + (x + z)`)`; ((y + Y)` + Y)`+ y = y by Th28; hence thesis by Th37; end; theorem Th41: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (((x + y`) + z)` + y)`` = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; (((x + y`) + z)` + y)` + (y` + y)` = (((x + y`) + z)` + y)` by Th32; hence thesis by Th36; end; theorem Th42: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + ((y + x`) + z)` = x proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; (((y + x`) + z)` + x)`` = x by Th41; hence thesis by Th25; end; theorem Th43: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x` + ((y + x) + z)` = x` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set X = x`; X + ((y + X`) + z)` = X by Th42; hence thesis by Th23; end; theorem Th44: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + y)` + x = x + y` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; set Z = x; x + (y + ((Z + y)` + x)`)` = (Z + y)` + x by Th38; hence thesis by Th28; end; theorem Th45: for L being satisfying_DN_1 non empty ComplLLattStr, x, y being Element of L holds (x + (x + y`)`)` = (x + y)` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y be Element of L; (x + ((x + y)` + x)`)` = (x + y)` by Th8; hence thesis by Th44; end; theorem Th46: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds ((x + y)` + (x + z))` + y = y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; ((x + y)` + ((x + y)` + (x + z)`)`)` = ((x + y)` + (x + z))` by Th45; hence thesis by Th40; end; theorem Th47: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = (x` + y)`` proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; ((((x + y)` + z)` + (x` + y)`)` + y)`` = (x` + y)`` by Th11; hence thesis by Th23; end; theorem Th48: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = x` + y proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; (((x + y)` + z)` + (x` + y)`)` + y = (x` + y)`` by Th47; hence thesis by Th23; end; theorem Th49: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)``+ (y + z) proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set X = (y + x)`, Y = (y + z), Z = x; (((X + Y)` + Z)` + (X` + Y)`)` + Y = X` + Y by Th48; hence thesis by Th46; end; theorem Th50: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + ( y + z) proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; (x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)`` + (y + z) by Th49; hence thesis by Th23; end; theorem Th51: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x) + (y + z) proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + (y + z) by Th50; hence thesis by Th23; end; theorem Th52: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x`` + (y + z) = (y + x) + (y + z) proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; x` + ((y + x) + (y + z))` = x` by Th43; hence thesis by Th51; end; theorem Th53: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x + y) + (x + z) = y + (x + z) proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; set Y = x, X = y; X`` + (Y + z) = (Y + X) + (Y + z) by Th52; hence thesis by Th23; end; theorem for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x + y) + (x + z) = z + (x + y) by Th53; theorem Th55: for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + (y + z) = z + (y + x) proof let L be satisfying_DN_1 non empty ComplLLattStr; let x, y, z be Element of L; (y + x) + (y + z) = z + (y + x) by Th53; hence thesis by Th53; end; theorem for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds x + (y + z) = y + (z + x) by Th55; theorem for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being Element of L holds (x + y) + z = x + (y + z) by Th55; Lm2: for L being satisfying_DN_1 non empty ComplLLattStr holds L is join-associative proof let L; for x, y, z holds (x + y) + z = x + (y + z) by Th55; hence thesis by LATTICES:def 5; end; Lm3: L is Robbins proof for x, y holds ((x + y)` + (x + y`)`)` = x by Th6; hence thesis by ROBBINS1:def 5; end; registration cluster satisfying_DN_1 -> join-associative for non empty ComplLLattStr; coherence by Lm2; cluster satisfying_DN_1 -> Robbins for non empty ComplLLattStr; coherence by Lm3; end; theorem Th58: for L being non empty ComplLLattStr, x, z being Element of L st L is join-commutative join-associative Huntington holds (z + x) *' (z + x`) = z proof let L be non empty ComplLLattStr; let x, z be Element of L; assume L is join-commutative join-associative Huntington; then reconsider L9 = L as join-commutative join-associative Huntington non empty ComplLLattStr; reconsider z9 = z, x9 = x as Element of L9; (z9 + x9) *' (z9 + x9`) = z9 + (x9 *' x9`) by ROBBINS1:31 .= z9 + Bot L9 by ROBBINS1:15 .= z9 by ROBBINS1:13; hence thesis; end; theorem Th59: for L being join-commutative join-associative non empty ComplLLattStr st L is Robbins holds L is satisfying_DN_1 proof let L be join-commutative join-associative non empty ComplLLattStr; assume L is Robbins; then reconsider L9 = L as join-commutative join-associative Robbins non empty ComplLLattStr; let x, y, z, u be Element of L; A1: L9 is Huntington; then A2: (z + x) *' (z + x`) = z by Th58; A3: ((x + y)` + z) *' z = (z + (x + y)`) *' z .= z *' (z + (x + y)`) .= z by A1,ROBBINS1:21; A4: (((x + y)` + z) *' x) + z = z + (((x + y)` + z) *' x) .= (z + ((x + y)` + z)) *' (z + x) by A1,ROBBINS1:31 .= (((x + y)` + z) + z) *' (z + x) .= ((x + y)` + (z + z)) *' (z + x) by LATTICES:def 5 .= ((x + y)` + z) *' (z + x) by A1,ROBBINS1:12 .= ((x` *' y`)`` + z) *' (z + x) by A1,ROBBINS1:17 .= ((x` *' y`) + z) *' (z + x) by A1,ROBBINS1:3 .= (z + (x` *' y`)) *' (z + x) .= ((z + x`) *' (z + y`)) *' (z + x) by A1,ROBBINS1:31 .= (z + x) *' ((z + x`) *' (z + y`)) .= (z + x) *' ((x` + z) *' (z + y`)) .= (z + x) *' ((x` + z) *' (y` + z)) .= (z + x) *' (x` + z) *' (y` + z) by A1,ROBBINS1:16 .= (z + x) *' (z + x`) *' (y` + z) .= z *' (z + y`) by A2 .= z by A1,ROBBINS1:21; (((x + y)` + z)` + (x + (z` + (z + u)`)`)`)` = (((x + y)` + z)`` *' (x + (z` + (z + u)`)`)``)`` by A1,ROBBINS1:17 .= ((x + y)` + z)`` *' (x + (z` + (z + u)`)`)`` by A1,ROBBINS1:3 .= ((x + y)` + z)`` *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:3 .= ((x + y)` + z) *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:3 .= ((x + y)`` *' z`)` *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:17 .= ((x + y) *' z`)` *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:3 .= ((x + y) *' z`)` *' (x + (z`` *' (z + u)``)``) by A1,ROBBINS1:17 .= ((x + y) *' z`)` *' (x + (z *' (z + u)``)``) by A1,ROBBINS1:3 .= ((x + y) *' z`)` *' (x + (z *' (z + u)``)) by A1,ROBBINS1:3 .= ((x + y) *' z`)` *' (x + (z *' (z + u))) by A1,ROBBINS1:3 .= ((x + y) *' z`)` *' (x + z) by A1,ROBBINS1:21 .= (((x + y) *' z`)` *' x) + (((x + y) *' z`)` *' z) by A1,ROBBINS1:30 .= (((x + y)`` *' z`)` *' x) + (((x + y) *' z`)` *' z) by A1,ROBBINS1:3 .= (((x + y)` + z) *' x) + (((x + y) *' z`)` *' z) by A1,ROBBINS1:17 .= (((x + y)` + z) *' x) + (((x + y)`` *' z`)` *' z) by A1,ROBBINS1:3 .= z by A1,A3,A4,ROBBINS1:17; hence thesis; end; registration cluster join-commutative join-associative Robbins -> satisfying_DN_1 for non empty ComplLLattStr; coherence by Th59; end; registration cluster satisfying_DN_1 de_Morgan for preOrthoLattice; existence proof take TrivOrtLat; thus thesis; end; end; registration cluster satisfying_DN_1 de_Morgan -> Boolean for preOrthoLattice; coherence; cluster Boolean -> satisfying_DN_1 for well-complemented preOrthoLattice; coherence; end; begin :: Meredith Two Axioms for Boolean Algebras definition let L be non empty ComplLLattStr; attr L is satisfying_MD_1 means for x, y being Element of L holds (x` + y)` + x = x; attr L is satisfying_MD_2 means for x, y, z being Element of L holds (x` + y)` + (z + y) = y + (z + x); end; Lm4: now let L be non empty ComplLLattStr; assume A1: L is satisfying_MD_1 satisfying_MD_2; A2: for x, y being Element of L holds x` + (x` + y) = x` + y proof let x, y be Element of L; set X = x` + y; X` + x = x by A1; hence thesis by A1; end; A3: for x, y being Element of L holds (x` + y)` + y = y + x proof let x, y be Element of L; set X = x` + y; A4: X` + (X` + y) = y + (X` + x) by A1; (x` + y)` + y = X` + (X` + y) by A2 .= y + x by A1,A4; hence thesis; end; A5: for x being Element of L holds x + x = x proof let x be Element of L; x + x = (x` + x)` + x by A3 .= x by A1; hence thesis; end; A6: for x, y being Element of L holds x + (x + y) = x + y proof let x, y be Element of L; x + (x + y) = (y` + x)` + (x + x) by A1 .= (y` + x)` + x by A5 .= x + y by A3; hence thesis; end; A7: for x, y being Element of L holds (x + y) + y = x + y proof let x, y be Element of L; set Y = x + y; (x + y) + y = (y` + (x + y))` + (x + y) by A3 .= (y` + (x + y))` + (x + (x + y)) by A6 .= Y + (x + y) by A1 .= x + y by A5; hence thesis; end; A8: for x, y being Element of L holds (x + y) + x = x + y proof let x, y be Element of L; (x + y) + x = ((y` + x)` + x) + x by A3 .= (y` + x)` + x by A7 .= x + y by A3; hence thesis; end; A9: for x, y being Element of L holds x + (y + (y + x)) = y + x proof let x, y be Element of L; set Z = y + x; x + (y + (y + x)) = (Z` + x)` + (y + x) by A1 .= y + x by A1; hence thesis; end; A10: for x, y being Element of L holds x + (y + x) = y + x proof let x, y be Element of L; x + (y + x) = x + (y + (y + x)) by A6 .= y + x by A9; hence thesis; end; A11: for x, y being Element of L holds (x + y`)` + y = y proof let x, y be Element of L; (x + y`)` + y = (y` + (x + y`))` + y by A10 .= y by A1; hence thesis; end; A12: for x being Element of L holds x`` + x = x proof let x be Element of L; (x` + x`)` + x = x by A1; hence thesis by A5; end; A13: for x being Element of L holds x + x`` = x proof let x be Element of L; x + x`` = (x`` + x) + x`` by A12 .= x`` + x by A8 .= x by A12; hence thesis; end; A14: for x, y being Element of L holds x + (x`` + y) = x + y proof let x, y be Element of L; x + (x`` + y) = (y` + x)` + (x`` + x) by A1 .= (y` + x)` + x by A12 .= x + y by A3; hence thesis; end; A15: for x being Element of L holds x + x```` = x proof let x be Element of L; x + x```` = x + (x`` + x````) by A14 .= x + x`` by A13 .= x by A13; hence thesis; end; A16: for x being Element of L holds x``` = x` proof let x be Element of L; x``` = (x + x````)` + x``` by A11 .= x` + x``` by A15 .= x` by A13; hence thesis; end; A17: for x, y, z being Element of L holds (x` + y)` + ((x` + z)` + y) = y + x proof let x, y, z be Element of L; (x` + y)` + ((x` + z)` + y) = y + ((x` + z)` + x) by A1 .= y + x by A1; hence thesis; end; A18: for x, y being Element of L holds x + y`` = x + y proof let x, y be Element of L; x + y = (y` + x)` + ((y` + x)` + x) by A17 .= (y` + x)` + ((y``` + x)` + x) by A16 .= (y``` + x)` + ((y``` + x)` + x) by A16 .= x + y`` by A17; hence thesis; end; A19: for x being Element of L holds x`` = x proof let x be Element of L; x`` = (x``` + x``)` + x`` by A1 .= (x` + x``)` + x`` by A16 .= (x` + x``)` + x by A18 .= x by A1; hence thesis; end; A20: for x, y, z being Element of L holds (x` + ((y + x)` + z)`)` + (y + ((y + x)` + z)`) = y + x proof let x, y, z be Element of L; set P = ((y + x)` + z)`; (x` + P)` + (y + P) = P + (y + x) by A1 .= y + x by A1; hence thesis; end; A21: for x, y being Element of L holds (x` + (x + y)`)` + (y` + (x + y)`) = y` + x proof let x, y be Element of L; (x` + (x + y)`)` + (y` + (x + y)`) = (x` + (x + y)`)` + (y` + ((y` + x)` + x)`) by A3 .= (x` + ((y` + x)` + x)`)` + (y` + ((y` + x)` + x)`) by A3 .= y` + x by A20; hence thesis; end; A22: for x, y being Element of L holds x + (x` + y)` = x proof let x, y be Element of L; x + (x` + y)` = ((x` + y)` + x) + (x` + y)` by A1 .= (x` + y)` + x by A8 .= x by A1; hence thesis; end; A23: for x, y being Element of L holds x` + (x + y)` = x` proof let x, y be Element of L; x` = x` + (x`` + y)` by A22 .= x` + (x + y)` by A19; hence thesis; end; A24: for x, y being Element of L holds x + (y + x`)` = x proof let x, y be Element of L; x + (y + x`)` = ((y + x`)` + x) + (y + x`)` by A11 .= (y + x`)` + x by A8 .= x by A11; hence thesis; end; A25: for x, y being Element of L holds x` + (y + x)` = x` proof let x, y be Element of L; x` = x` + (y + x``)` by A24 .= x` + (y + x)` by A19; hence thesis; end; A26: for x, y being Element of L holds x + y` = y` + x proof let x, y be Element of L; y` + x = (x` + (x + y)`)` + (y` + (x + y)`) by A21 .= x`` + (y` + (x + y)`) by A23 .= x`` + y` by A25 .= x + y` by A19; hence thesis; end; A27: for x, y being Element of L holds x + y = y + x proof let x, y be Element of L; y`` = y by A19; hence thesis by A26; end; hence L is join-commutative by LATTICES:def 4; A28: for x, y, z being Element of L holds ((x` + y)` + z)` + (x` + z) = z + ( x` + y) proof let x, y, z be Element of L; ((x` + y)` + z)` + (x` + z) = z + (x` + (x` + y)) by A1 .= z + (x` + y) by A2; hence thesis; end; A29: for x, y being Element of L holds x + (y` + x) = y` + x proof let x, y be Element of L; x + (y` + x) = ((y` + x)` + x)` + (y` + x) by A28 .= y` + x by A1; hence thesis; end; A30: for x, y being Element of L holds (x + y)` + x = y` + x proof let x, y be Element of L; set Y = y` + x; y` + x = x + (y` + x) by A29 .= (Y` + x)` + x by A3 .= (x + y)` + x by A3; hence thesis; end; A31: for x, y being Element of L holds (x + y)` + (y` + x)` = x` + (y` + x)` proof let x, y be Element of L; (x + y)` + (y` + x)` = ((y` + x)` + x)` + (y` + x)` by A3 .= x` + (y` + x)` by A30; hence thesis; end; for x, y being Element of L holds (x` + y`)` + (x` + y)` = x proof let x, y be Element of L; (x` + y`)` + (x` + y)` = (y` + x`)` + (x` + y)` by A27 .= (x` + y)` + (y` + x`)` by A27 .= x`` + (y` + x`)` by A31 .= x + (y` + x`)` by A19 .= x by A24; hence thesis; end; hence L is Huntington by ROBBINS1:def 6; A32: for x, y, z being Element of L holds (x + y) + (y + z) = (x + y) + z proof let x, y, z be Element of L; set Y = x + y; (x + y) + z = (z` + Y)` + Y by A3 .= (z` + Y)` + (y + Y) by A10 .= Y + (y + z) by A1; hence thesis; end; for x, y, z being Element of L holds (x + y) + z = x + (y + z) proof let x, y, z be Element of L; for x, y, z being Element of L holds (x + y) + (z + x) = y + (x + z) proof let x, y, z be Element of L; (x + y) + (z + x) = (z + x) + (x + y) by A27 .= (z + x) + y by A32 .= (x + z) + y by A27 .= y + (x + z) by A27; hence thesis; end; then (y + x) + (z + y) = x + (y + z); then A33: (x + y) + (z + y) = x + (y + z) by A27; (x + y) + z = (x + y) + (y + z) by A32 .= x + (y + z) by A27,A33; hence thesis; end; hence L is join-associative by LATTICES:def 5; end; registration cluster satisfying_MD_1 satisfying_MD_2 -> join-commutative join-associative Huntington for non empty ComplLLattStr; coherence by Lm4; cluster join-commutative join-associative Huntington -> satisfying_MD_1 satisfying_MD_2 for non empty ComplLLattStr; coherence proof let L be non empty ComplLLattStr; assume L is join-commutative join-associative Huntington; then reconsider L9 = L as join-commutative join-associative Huntington non empty ComplLLattStr; A1: L9 is satisfying_MD_2 proof let x, y, z be Element of L9; set Z = z + y; A2: Z + y` = z + (y + y`) by LATTICES:def 5 .= z + Top L9 by ROBBINS1:def 8 .= Top L9 by ROBBINS1:19; (x` + y)` + (z + y) = (x` + y``)` + (z + y) by ROBBINS1:3 .= (x *' y`) + (z + y) by ROBBINS1:def 4 .= (Z + x) *' (Z + y`) by ROBBINS1:31 .= Z + x by A2,ROBBINS1:14 .= y + (z + x) by LATTICES:def 5; hence thesis; end; L9 is satisfying_MD_1 proof let x, y be Element of L9; (x` + y)` + x = (x` + y``)` + x by ROBBINS1:3 .= (x *' y`) + x by ROBBINS1:def 4 .= x by ROBBINS1:20; hence thesis; end; hence thesis by A1; end; end; registration cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan for preOrthoLattice; existence proof take TrivOrtLat; thus thesis; end; end; registration cluster satisfying_MD_1 satisfying_MD_2 de_Morgan -> Boolean for preOrthoLattice; coherence; cluster Boolean -> satisfying_MD_1 satisfying_MD_2 for well-complemented preOrthoLattice; coherence; end;