:: Short {S}heffer Stroke-Based Single Axiom for {B}oolean Algebras :: by Aneta {\L}ukaszuk and Adam Grabowski :: :: Received May 31, 2004 :: Copyright (c) 2004-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SHEFFER1, SUBSET_1, RELAT_1, ZFMISC_1, LATTICES, ROBBINS1, EQREL_1, SHEFFER2; notations STRUCT_0, LATTICES, ROBBINS1, SHEFFER1; constructors SHEFFER1; registrations LATTICES, SHEFFER1, STRUCT_0; begin :: First Implication definition let L be non empty ShefferStr; attr L is satisfying_Sh_1 means :: SHEFFER2:def 1 for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | x)) = y; end; registration cluster trivial -> satisfying_Sh_1 for non empty ShefferStr; end; registration cluster satisfying_Sh_1 satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for non empty ShefferStr; end; reserve L for satisfying_Sh_1 non empty ShefferStr; theorem :: SHEFFER2:1 for x, y, z, u being Element of L holds ((x | (y | z)) | (x | (x | (y | z)))) | ((z | ((x | z) | z)) | (u | (x | (y | z)))) = z | ((x | z) | z); theorem :: SHEFFER2:2 for x, y, z being Element of L holds ((x | y) | (((y | ((z | y) | y)) | (x | y)) | (x | y))) | z = y | ((z | y) | y); theorem :: SHEFFER2:3 for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | ( z | ((x | z) | z))) = y; theorem :: SHEFFER2:4 for x, y being Element of L holds x | ((x | ((x | x) | x)) | (y | (x | ((x | x) | x)))) = x | ((x |x) | x); theorem :: SHEFFER2:5 for x being Element of L holds x | ((x | x) | x) = x | x; theorem :: SHEFFER2:6 for x being Element of L holds (x | ((x | x) | x )) | (x | x) = x; theorem :: SHEFFER2:7 for x, y being Element of L holds (x | x) | (x | (y | x)) = x; theorem :: SHEFFER2:8 for x, y being Element of L holds (x | (((y | y) | x) | x)) | y = y | y; theorem :: SHEFFER2:9 for x, y being Element of L holds ((x | y) | (((x | y) | (x | y)) | (x | y))) | ((x | y) | (x | y)) = y | ((((x | y) | (x | y )) | y) | y); theorem :: SHEFFER2:10 for x, y being Element of L holds x | ((((y | x) | (y | x)) | x ) | x) = y | x; theorem :: SHEFFER2:11 for x, y being Element of L holds (x | x) | (y | x) = x; theorem :: SHEFFER2:12 for x, y being Element of L holds x | (y | (x | x)) = x | x; theorem :: SHEFFER2:13 for x, y being Element of L holds ((x | y) | (x | y)) | y = x | y; theorem :: SHEFFER2:14 for x, y being Element of L holds x | ((y | x) | x) = y | x; theorem :: SHEFFER2:15 for x, y, z being Element of L holds (x | y) | (x | (z | y)) = x; theorem :: SHEFFER2:16 for x, y, z being Element of L holds (x | (y | z)) | (x | z) = x; theorem :: SHEFFER2:17 for x, y, z being Element of L holds x | ((x | y) | (z | y)) = x | y; theorem :: SHEFFER2:18 for x, y, z being Element of L holds ((x | (y | z)) | z) | x = x | (y | z); theorem :: SHEFFER2:19 for x, y being Element of L holds x | ((y | x) | x) = x | y; theorem :: SHEFFER2:20 for x, y being Element of L holds x | y = y | x; theorem :: SHEFFER2:21 for x, y being Element of L holds (x | y) | (x | x) = x; theorem :: SHEFFER2:22 for x, y, z being Element of L holds (x | y) | (y | (z | x)) = y; theorem :: SHEFFER2:23 for x, y, z being Element of L holds (x | (y | z)) | (z | x) = x; theorem :: SHEFFER2:24 for x, y, z being Element of L holds (x | y) | (y | (x | z)) = y; theorem :: SHEFFER2:25 for x, y, z being Element of L holds (x | (y | z)) | (y | x) = x; theorem :: SHEFFER2:26 for x, y, z being Element of L holds ((x | y) | (x | z)) | z = x | z; theorem :: SHEFFER2:27 for x, y, z being Element of L holds x | (y | (x | (y | z))) = x | (y | z); theorem :: SHEFFER2:28 for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (x | z); theorem :: SHEFFER2:29 for x, y, z, u being Element of L holds (x | (y | z))| (x | (u | (y | x))) = (x | (y | z)) | (y | x); theorem :: SHEFFER2:30 for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (z | x); theorem :: SHEFFER2:31 for x, y, z, u being Element of L holds (x | (y | z)) | (x | (u | (y | x))) = x; theorem :: SHEFFER2:32 for x, y being Element of L holds x | (y | (x | y)) = x | x; theorem :: SHEFFER2:33 for x, y, z being Element of L holds x | (y | z) = x | (z | y); theorem :: SHEFFER2:34 for x, y, z being Element of L holds x | (y | (x | (z | (y | x)) )) = x | x; theorem :: SHEFFER2:35 for x, y, z being Element of L holds (x | (y | z)) | ((y |x) | x ) = (x | (y | z)) | (x | (y | z)); theorem :: SHEFFER2:36 for x, y being Element of L holds (x | (y | x)) | y = y | y; theorem :: SHEFFER2:37 for x, y, z being Element of L holds (x | y) | z = z | (y | x); theorem :: SHEFFER2:38 for x, y, z being Element of L holds x | (y | (z | (x | y))) = x | (y | y); theorem :: SHEFFER2:39 for x, y, z being Element of L holds ((x | y) | y) | (y | (z | x )) = (y | (z | x)) | (y | (z | x)); theorem :: SHEFFER2:40 for x, y, z, u being Element of L holds (x | y) | (z | u) = (u | z) | (y | x) ; theorem :: SHEFFER2:41 for x, y, z being Element of L holds x | (y | ((y | x) | z)) = x | (y | y); theorem :: SHEFFER2:42 for x, y being Element of L holds x | (y | x) = x | (y | y); theorem :: SHEFFER2:43 for x, y being Element of L holds (x | y) | y = y | (x | x); theorem :: SHEFFER2:44 for x, y being Element of L holds x | (y | y) = x | (x | y); theorem :: SHEFFER2:45 for x, y, z being Element of L holds (x | (y | y)) | (x | (z | y )) = (x | (z | y)) | (x | (z | y)); theorem :: SHEFFER2:46 for x, y, z being Element of L holds (x | (y | z)) | (x | (y | y )) = (x | (y | z)) | (x | (y | z)); theorem :: SHEFFER2:47 for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x | y)))) = x | ((y | y) | (y | y)); theorem :: SHEFFER2:48 for x, y, z being Element of L holds ((x | (y | z)) | (x | (y | z))) | (y | y) = x | (y | y); theorem :: SHEFFER2:49 for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x | y)))) = x | y; theorem :: SHEFFER2:50 for x, y, z being Element of L holds (((x | y) | (x | y)) | ((z | ((x | y) | z)) | (x | y))) | (x | x) = (z | ((x | y) | z)) | (x | x); theorem :: SHEFFER2:51 for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = (y | z) | (y | y); theorem :: SHEFFER2:52 for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = y; theorem :: SHEFFER2:53 for x, y, z being Element of L holds x | ((y | ((x | z) | y)) | x) = y | ((x | z) | y); theorem :: SHEFFER2:54 for x, y, z being Element of L holds x | ((y | (y | (z | x))) | x) = y | ((x | (y | (x | z))) | y); theorem :: SHEFFER2:55 for x, y, z being Element of L holds x | ((y | (y | (z | x))) | x) = y | (y | (z | x)); theorem :: SHEFFER2:56 for x, y, z, u being Element of L holds x | (y | (z | (z | (u | (y | x))))) = x | (y | y); theorem :: SHEFFER2:57 for x, y, z being Element of L holds x | (y | (y | (z | (x | y)) )) = x | (y | (x | x)); theorem :: SHEFFER2:58 for x, y, z being Element of L holds x | (y | (y | (z | (x | y)) )) = x | x; theorem :: SHEFFER2:59 for x, y being Element of L holds x | (y | (y | y)) = x | x; theorem :: SHEFFER2:60 for x, y, z being Element of L holds x | (((y | (z | x)) | (y | (z | x))) | (z | z)) = x | (y | (z | x)); theorem :: SHEFFER2:61 for x, y, z being Element of L holds x | (y | (z | z)) = x | (y | (z | x)); theorem :: SHEFFER2:62 for x, y, z being Element of L holds x | (y | ((z | z) | x)) = x | (y | z); theorem :: SHEFFER2:63 for x, y, z being Element of L holds (x | (y | y)) | (x | (z | ( (y | y) | x))) = (x | (z | y)) | (x | (z | y)); theorem :: SHEFFER2:64 for x, y, z being Element of L holds (x | (y | y)) | (x | (z | ( x | (y | y)))) = (x | (z | y)) | (x | (z |y)); theorem :: SHEFFER2:65 for x, y, z being Element of L holds (x | (y | y)) | (x | (z | z )) = (x | (z | y)) | (x | (z | y)); theorem :: SHEFFER2:66 for x, y, z being Element of L holds ((x | x) | y) | ((z | z) | y) = (y | (x | z)) | (y | (x | z)); theorem :: SHEFFER2:67 for L being non empty ShefferStr st L is satisfying_Sh_1 holds L is satisfying_Sheffer_1; theorem :: SHEFFER2:68 for L being non empty ShefferStr st L is satisfying_Sh_1 holds L is satisfying_Sheffer_2; theorem :: SHEFFER2:69 for L being non empty ShefferStr st L is satisfying_Sh_1 holds L is satisfying_Sheffer_3; registration cluster properly_defined Boolean well-complemented Lattice-like de_Morgan satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 for non empty ShefferOrthoLattStr; end; registration cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined -> Boolean Lattice-like for non empty ShefferOrthoLattStr; cluster Boolean Lattice-like well-complemented properly_defined -> satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for non empty ShefferOrthoLattStr; end; begin :: Second Implication reserve L for satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 non empty ShefferStr; reserve v,q,p,w,z,y,x for Element of L; theorem :: SHEFFER2:70 for x,w holds w | ((x | x) | x) = w | w; theorem :: SHEFFER2:71 for p,x holds x = (x | x) | (p | (p | p)); theorem :: SHEFFER2:72 for y,w holds (w | w) | (w | (y | (y | y))) = w; theorem :: SHEFFER2:73 for q,p,y,w holds (((w | (y | (y | y))) | p) | ((q | q) | p)) = ((p | (w | q)) | (p | (w | q))); theorem :: SHEFFER2:74 for q,p,x holds (x | p) | ((q | q) | p) = ((p | ((x | x) | q)) | (p | ((x | x) | q))); theorem :: SHEFFER2:75 for w,p,y,q holds (((w | w) | p) | ((q | (y | (y | y))) | p)) = ((p | (w | q)) | (p | (w | q))); theorem :: SHEFFER2:76 for p,x holds x = (x | x) | ((p | p) | p); theorem :: SHEFFER2:77 for y,w holds (w | w) | (w | ((y | y) | y)) = w; theorem :: SHEFFER2:78 for y,w holds ((w | ((y | y) | y)) | (w | w)) = w; theorem :: SHEFFER2:79 for p,y,w holds ((w | ((y | y) | y)) | (p | (p | p))) = w; theorem :: SHEFFER2:80 for p,x,y holds (((y | (x | x)) | (y | (x | x))) | (p | (p | p)) ) = ((x | x) | y); theorem :: SHEFFER2:81 for x,y holds y | (x | x) = (x | x) | y; theorem :: SHEFFER2:82 for y,w holds w | y = ((y | y) | (y | y)) | w; theorem :: SHEFFER2:83 for y,w holds w | y = y | w; theorem :: SHEFFER2:84 for x,p holds (p | x) | (p | ((x | x) | (x | x))) = (((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p); theorem :: SHEFFER2:85 for x,p holds (p | x) | (p | x) = (((x | x) | (x | x)) | p) | (( (x | x) | (x | x)) | p); theorem :: SHEFFER2:86 for x,p holds (p | x) | (p | x) = (x | p) | (((x | x) | (x | x)) | p); theorem :: SHEFFER2:87 for x,p holds (p | x) | (p | x) = (x | p) | (x | p); theorem :: SHEFFER2:88 for y,q,w holds ((w | q) | ((y | y) | y)) | ((w | q) | (w | q)) = ((w | w) | (w | q)) | ((q | q) | (w | q)); theorem :: SHEFFER2:89 for q,w holds w | q = ((w | w) | (w | q)) | ((q | q) | (w | q)); theorem :: SHEFFER2:90 for q,p holds ((p | p) | (p | ((q | q) | q))) = ((((q | q) | (q | q)) | p) | ((q | q) | p)); theorem :: SHEFFER2:91 for p,q holds p = ((((q | q) | (q | q)) | p) | ((q | q) | p)); theorem :: SHEFFER2:92 for p,q holds p = (q | p) | ((q | q) | p); theorem :: SHEFFER2:93 for z,w,x holds ((((x | x) | w) | ((z | z) | w)) | ((w | (x | z) ) | (w | (x | z)))) = (((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w | (x | z)))); theorem :: SHEFFER2:94 for z,w,x holds ((((x | x) | w) | ((z | z) | w)) | ((w | (x | z) ) | (w | (x | z)))) = (w | (x | z)); theorem :: SHEFFER2:95 for w,p holds ((p | p) | (p | (w | (w | w)))) = (((w | w) | p) | (((w | w) | (w | w)) | p)); theorem :: SHEFFER2:96 for p,w holds p = ((w | w) | p) | (((w | w) | (w | w)) | p); theorem :: SHEFFER2:97 for p,w holds p = (((w | w) | p) | (w | p)); theorem :: SHEFFER2:98 for z,q,x holds ((((x | x) | q) | ((z | z) | q)) | ((q | (x | z) ) | (q | (x | z)))) = ((((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q))); theorem :: SHEFFER2:99 for q,z,x holds (q | (x | z)) = ((((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q))); theorem :: SHEFFER2:100 for q,z,x holds (q | (x | z)) = ((z | ((x | x) | q)) | ((q | q) | ((x | x) | q))); theorem :: SHEFFER2:101 for w,y holds w | w = ((y | y) | y) | w; theorem :: SHEFFER2:102 for w,p holds ((p | w) | ((w | w) | p)) = p; theorem :: SHEFFER2:103 for y,w holds ((w | w) | ((w | w) | ((y | y) | y))) = (y | y) | y; theorem :: SHEFFER2:104 for y,w holds (w | w) | w = (y | y) | y; theorem :: SHEFFER2:105 for p,w holds (w | p) | (p | (w | w)) = p; theorem :: SHEFFER2:106 for w,p holds (p | (w | w)) | (w | p) = p; theorem :: SHEFFER2:107 for p,w holds (w | p) | (w | (p | p)) = w; theorem :: SHEFFER2:108 for x,y holds (y | (((y | (x | x)) | (y | (x | x))) | (x | y))) = x | y; theorem :: SHEFFER2:109 for p,w holds (w | (p | p)) | (w | p) = w; theorem :: SHEFFER2:110 for p,w,q,y holds (((y | y) | y) | q) | ((w | w) | q) = (q | (( (p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w)); theorem :: SHEFFER2:111 for q,w,p holds (q | q) | ((w | w) | q) = (q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w)); theorem :: SHEFFER2:112 for w,y,p holds (w | p) | (w | (p | (y | (y | y)))) = w; theorem :: SHEFFER2:113 for w,y,p holds (w | (p | (y | (y | y)))) | (w | p) = w; theorem :: SHEFFER2:114 for q,p,y holds (((y | y) | y) | p) | ((q | q) | p) = (p | ((p | p) | q)) | (p | ((p | p) | q)); theorem :: SHEFFER2:115 for q,z,x holds (((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q))) = ((((z | z) | (z | z)) | (x | q)) | ((q | q) | (x | q))); theorem :: SHEFFER2:116 for q,z,x holds (((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q))) = ((z | (x | q)) | ((q | q) | (x | q))); theorem :: SHEFFER2:117 for w,q,z holds (((w | w) | ((z | z) | q)) | ((q | ((q | q) | z )) | (q | ((q | q) | z)))) = (((z | z) | q) | (w | q)) | (((z | z) | q) | (w | q)); theorem :: SHEFFER2:118 for q,p,x holds (((p | (x | p)) | (p | (x | p))) | (q | (q | q) )) = (x | x) | p; theorem :: SHEFFER2:119 for p,x holds p | (x | p) = (x | x) | p; theorem :: SHEFFER2:120 for p,y holds (y | p) | ((y | y) | p) = (p | p) | (y | p); theorem :: SHEFFER2:121 for x,y holds x = (x | x) | (y | x); theorem :: SHEFFER2:122 for x,y holds (y | x) | x = ((x | (y | y)) | (x | (y | y))) | ( y | x); theorem :: SHEFFER2:123 for x,z,y holds (((x | ((y | y) | z)) | (x | ((y | y) | z))) | ((y | x) | ((z | z) | x))) = (z | (y | x)) | x; theorem :: SHEFFER2:124 for x,y,z holds ((x | (((z | (z | z)) | (z | (z | z))) | y)) | (x | (((z | (z | z)) | (z | (z | z))) | y))) = x; theorem :: SHEFFER2:125 for x,z,y holds (x | ((y | y) | z)) | z = z | (y | x); theorem :: SHEFFER2:126 for x,y holds x | ((y | x) | x) = y | x; theorem :: SHEFFER2:127 for z,y,x holds y = (((x | x) | x) | y) | ((z | z) | y); theorem :: SHEFFER2:128 for z,y holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y; theorem :: SHEFFER2:129 for x,z,y holds (((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z)) = ((x | x) | ((y | y) | z)) | z; theorem :: SHEFFER2:130 for x,z,y holds ((((y | y) | z) | (x | z)) | (((y | y) | z) | ( x | z))) = z | (y | (x | x)); theorem :: SHEFFER2:131 for y,x holds ((x | y) | (x | y)) | x = x | y; theorem :: SHEFFER2:132 for p,w holds (w | w) | (w | p) = w; theorem :: SHEFFER2:133 for w,p holds (p | w) | (w | w) = w; theorem :: SHEFFER2:134 for p,y,w holds (w | (y | (y | y))) | (w | p) = w; theorem :: SHEFFER2:135 for p,w holds ((w | p) | (w | w)) = w; theorem :: SHEFFER2:136 for y,p,w holds (w | p) | (w | (y | (y | y))) = w; theorem :: SHEFFER2:137 for p,q,w,y,x holds ((((x | (y | (y | y))) | w) | ((q | q) | w) ) | ((w | (x | q)) | (w | (x | q)))) = (((w | (p | (p | p))) | (w | (x | q))) | (((x | q) | (x | q)) | (w | (x | q)))); theorem :: SHEFFER2:138 for q,w,y,x holds ((((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q)))) = (w | (((x | q) | (x | q)) | (w | (x | q))) ); theorem :: SHEFFER2:139 for q,w,y,x holds (((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q))) = w | (x | q); theorem :: SHEFFER2:140 for z,p,q,y,x holds ((((x | (y | (y | y))) | q) | ((z | z) | q) ) | ((q | (x | z)) | (q | (x | z)))) = ((((z | z) | (p | (p | p))) | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q))); theorem :: SHEFFER2:141 for z,p,q,y,x holds q | (x | z) = (((z | z) | (p | (p | p))) | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q)); theorem :: SHEFFER2:142 for z,q,y,x holds q | (x | z) = (z | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q)); theorem :: SHEFFER2:143 for v,p,y,x holds p | (x | v) = (v | ((x | (y | (y | y))) | p)) | p; theorem :: SHEFFER2:144 for y,w,z,v,x holds ((w | (z | (x | v))) | (((x | (y | (y | y)) ) | z) | ((v | v) | z))) = z | (x | v); theorem :: SHEFFER2:145 for y,z,x holds ((y | ((x | x) | z)) | (y | ((x | x) | z))) | ( (x | y) | ((z | z) | y)) = y | ((x | x) | z); theorem :: SHEFFER2:146 for z,y,x holds (z | (x | y)) | y = y | ((x | x) | z); theorem :: SHEFFER2:147 for x,w,y,z holds ((((x | x) | w) | ((z | (y | (y | y))) | w)) | w) = w | (x | z); theorem :: SHEFFER2:148 for z,w,x holds (w | (z | ((x | x) | w))) = w | (x | z); theorem :: SHEFFER2:149 for p,z,y,x holds (((z | (x | p)) | (z | (x | p))) | (((x | (y | (y | y))) | z) | ((p | p) | z))) = ((((p | p) | z) | ((x | (y | (y | y))) | z )) | (((p | p) | z) | ((x | (y | (y | y))) | z))); theorem :: SHEFFER2:150 for p,z,y,x holds (z | (x | p)) = ((((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z))); theorem :: SHEFFER2:151 for z,p,y,x holds z | (x | p) = z | (p | ((x | (y | (y | y))) | (x | (y | (y | y))))); theorem :: SHEFFER2:152 for z,p,x holds z | (x | p) = z | (p | x); theorem :: SHEFFER2:153 for w,q,p holds (p | q) | w = w | (q | p); theorem :: SHEFFER2:154 for w,p,q holds ((q | p) | w) | q = q | ((p | p) | w); theorem :: SHEFFER2:155 for z,w,y,x holds w | x = (w | ((x | z) | (((x | (y | (y | y))) | (x | (y | (y | y)))) | w))); theorem :: SHEFFER2:156 for w,z,x holds w | x = w | ((x | z) | (x | w)); theorem :: SHEFFER2:157 for q,x,z,y holds ((x | y) | (((x | (y | (z | (z | z)))) | q) | x)) = ((x | y) | (x | (y | (z | (z | z))))); theorem :: SHEFFER2:158 for x,q,z,y holds ((x | y) | (x | (((y | (z | (z | z))) | (y | (z | (z | z)))) | q))) = ((x | y) | (x | (y | (z | (z | z))))); theorem :: SHEFFER2:159 for z,x,q,y holds (x | y) | (x | (y | q)) = ((x | y) | (x | (y | (z | (z | z))))); theorem :: SHEFFER2:160 for x,q,y holds (x | y) | (x | (y | q)) = x; theorem :: SHEFFER2:161 L is satisfying_Sh_1; registration cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 -> satisfying_Sh_1 for non empty ShefferStr; cluster satisfying_Sh_1 -> satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for non empty ShefferStr; end; registration cluster satisfying_Sh_1 properly_defined -> Boolean Lattice-like for non empty ShefferOrthoLattStr; cluster Boolean Lattice-like well-complemented properly_defined -> satisfying_Sh_1 for non empty ShefferOrthoLattStr; end;