:: 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-2012 Association of Mizar Users


begin

definition
let L be non empty ShefferStr ;
attrL is satisfying_Sh_1  means :Def1: :: SHEFFER2:def 1
 for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | x)) = y;
end;

:: deftheorem Def1 defines satisfying_Sh_1 SHEFFER2:def_1_:_
 for L being non empty ShefferStr holds
( L is satisfying_Sh_1 iff for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | x)) = y );

registration
cluster non empty trivial  ->  non empty satisfying_Sh_1 for ShefferStr ;
coherence
 for b1 being non empty ShefferStr st b1 is trivial holds
b1 is satisfying_Sh_1
proofend;
end;

registration
cluster non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 for ShefferStr ;
existence
 ex b1 being non empty ShefferStr st
( b1 is satisfying_Sh_1 & b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 )
proofend;
end;

theorem Th1: :: SHEFFER2:1
for L being non empty satisfying_Sh_1 ShefferStr
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)
proofend;

theorem Th2: :: SHEFFER2:2
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | y) | (((y | ((z | y) | y)) | (x | y)) | (x | y))) | z = y | ((z | y) | y)
proofend;

theorem Th3: :: SHEFFER2:3
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | ((x | z) | z))) = y
proofend;

theorem Th4: :: SHEFFER2:4
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | ((x | ((x | x) | x)) | (y | (x | ((x | x) | x)))) = x | ((x | x) | x)
proofend;

theorem Th5: :: SHEFFER2:5
for L being non empty satisfying_Sh_1 ShefferStr
for x being Element of L holds x | ((x | x) | x) = x | x
proofend;

theorem Th6: :: SHEFFER2:6
for L being non empty satisfying_Sh_1 ShefferStr
for x being Element of L holds (x | ((x | x) | x)) | (x | x) = x
proofend;

theorem Th7: :: SHEFFER2:7
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | x) | (x | (y | x)) = x
proofend;

theorem Th8: :: SHEFFER2:8
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | (((y | y) | x) | x)) | y = y | y
proofend;

theorem Th9: :: SHEFFER2:9
for L being non empty satisfying_Sh_1 ShefferStr
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)
proofend;

theorem Th10: :: SHEFFER2:10
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | ((((y | x) | (y | x)) | x) | x) = y | x
proofend;

theorem Th11: :: SHEFFER2:11
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | x) | (y | x) = x
proofend;

theorem Th12: :: SHEFFER2:12
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | (y | (x | x)) = x | x
proofend;

theorem Th13: :: SHEFFER2:13
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds ((x | y) | (x | y)) | y = x | y
proofend;

theorem Th14: :: SHEFFER2:14
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | ((y | x) | x) = y | x
proofend;

theorem Th15: :: SHEFFER2:15
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | y) | (x | (z | y)) = x
proofend;

theorem Th16: :: SHEFFER2:16
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | z)) | (x | z) = x
proofend;

theorem Th17: :: SHEFFER2:17
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((x | y) | (z | y)) = x | y
proofend;

theorem Th18: :: SHEFFER2:18
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | (y | z)) | z) | x = x | (y | z)
proofend;

theorem Th19: :: SHEFFER2:19
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | ((y | x) | x) = x | y
proofend;

theorem Th20: :: SHEFFER2:20
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | y = y | x
proofend;

theorem Th21: :: SHEFFER2:21
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | y) | (x | x) = x
proofend;

theorem Th22: :: SHEFFER2:22
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | y) | (y | (z | x)) = y
proofend;

theorem Th23: :: SHEFFER2:23
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | z)) | (z | x) = x
proofend;

theorem Th24: :: SHEFFER2:24
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | y) | (y | (x | z)) = y
proofend;

theorem Th25: :: SHEFFER2:25
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | z)) | (y | x) = x
proofend;

theorem Th26: :: SHEFFER2:26
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | y) | (x | z)) | z = x | z
proofend;

theorem Th27: :: SHEFFER2:27
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (x | (y | z))) = x | (y | z)
proofend;

theorem Th28: :: SHEFFER2:28
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (x | z)
proofend;

theorem Th29: :: SHEFFER2:29
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z, u being Element of L holds (x | (y | z)) | (x | (u | (y | x))) = (x | (y | z)) | (y | x)
proofend;

theorem Th30: :: SHEFFER2:30
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (z | x)
proofend;

theorem Th31: :: SHEFFER2:31
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z, u being Element of L holds (x | (y | z)) | (x | (u | (y | x))) = x
proofend;

theorem Th32: :: SHEFFER2:32
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | (y | (x | y)) = x | x
proofend;

theorem Th33: :: SHEFFER2:33
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | z) = x | (z | y)
proofend;

theorem Th34: :: SHEFFER2:34
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (x | (z | (y | x)))) = x | x
proofend;

theorem Th35: :: SHEFFER2:35
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | z)) | ((y | x) | x) = (x | (y | z)) | (x | (y | z))
proofend;

theorem Th36: :: SHEFFER2:36
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | (y | x)) | y = y | y
proofend;

theorem Th37: :: SHEFFER2:37
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | y) | z = z | (y | x)
proofend;

theorem Th38: :: SHEFFER2:38
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (z | (x | y))) = x | (y | y)
proofend;

theorem Th39: :: SHEFFER2:39
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | y) | y) | (y | (z | x)) = (y | (z | x)) | (y | (z | x))
proofend;

theorem Th40: :: SHEFFER2:40
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z, u being Element of L holds (x | y) | (z | u) = (u | z) | (y | x)
proofend;

theorem Th41: :: SHEFFER2:41
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | ((y | x) | z)) = x | (y | y)
proofend;

theorem Th42: :: SHEFFER2:42
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | (y | x) = x | (y | y)
proofend;

theorem Th43: :: SHEFFER2:43
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | y) | y = y | (x | x)
proofend;

theorem Th44: :: SHEFFER2:44
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | (y | y) = x | (x | y)
proofend;

theorem Th45: :: SHEFFER2:45
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | y)) = (x | (z | y)) | (x | (z | y))
proofend;

theorem Th46: :: SHEFFER2:46
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | z)) | (x | (y | y)) = (x | (y | z)) | (x | (y | z))
proofend;

theorem Th47: :: SHEFFER2:47
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x | y)))) = x | ((y | y) | (y | y))
proofend;

theorem Th48: :: SHEFFER2:48
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | (y | z)) | (x | (y | z))) | (y | y) = x | (y | y)
proofend;

theorem Th49: :: SHEFFER2:49
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x | y)))) = x | y
proofend;

theorem Th50: :: SHEFFER2:50
for L being non empty satisfying_Sh_1 ShefferStr
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)
proofend;

theorem Th51: :: SHEFFER2:51
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = (y | z) | (y | y)
proofend;

theorem Th52: :: SHEFFER2:52
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = y
proofend;

theorem Th53: :: SHEFFER2:53
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((y | ((x | z) | y)) | x) = y | ((x | z) | y)
proofend;

theorem Th54: :: SHEFFER2:54
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((y | (y | (z | x))) | x) = y | ((x | (y | (x | z))) | y)
proofend;

theorem Th55: :: SHEFFER2:55
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((y | (y | (z | x))) | x) = y | (y | (z | x))
proofend;

theorem Th56: :: SHEFFER2:56
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z, u being Element of L holds x | (y | (z | (z | (u | (y | x))))) = x | (y | y)
proofend;

theorem Th57: :: SHEFFER2:57
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (y | (z | (x | y)))) = x | (y | (x | x))
proofend;

theorem Th58: :: SHEFFER2:58
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (y | (z | (x | y)))) = x | x
proofend;

theorem Th59: :: SHEFFER2:59
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | (y | (y | y)) = x | x
proofend;

theorem Th60: :: SHEFFER2:60
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (((y | (z | x)) | (y | (z | x))) | (z | z)) = x | (y | (z | x))
proofend;

theorem Th61: :: SHEFFER2:61
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (z | z)) = x | (y | (z | x))
proofend;

theorem Th62: :: SHEFFER2:62
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | ((z | z) | x)) = x | (y | z)
proofend;

theorem Th63: :: SHEFFER2:63
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | ((y | y) | x))) = (x | (z | y)) | (x | (z | y))
proofend;

theorem Th64: :: SHEFFER2:64
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | (x | (y | y)))) = (x | (z | y)) | (x | (z | y))
proofend;

theorem Th65: :: SHEFFER2:65
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | z)) = (x | (z | y)) | (x | (z | y))
proofend;

theorem Th66: :: SHEFFER2:66
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | x) | y) | ((z | z) | y) = (y | (x | z)) | (y | (x | z))
proofend;

theorem Th67: :: SHEFFER2:67
for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_1
proofend;

theorem Th68: :: SHEFFER2:68
for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_2
proofend;

theorem Th69: :: SHEFFER2:69
for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_3
proofend;

registration
cluster non empty Lattice-like Boolean well-complemented de_Morgan properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 for ShefferOrthoLattStr ;
existence
 ex b1 being non empty ShefferOrthoLattStr st
( b1 is properly_defined & b1 is Boolean & b1 is well-complemented & b1 is Lattice-like & b1 is de_Morgan & b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 & b1 is satisfying_Sh_1 )
proofend;
end;

registration
cluster non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3  ->  non empty Lattice-like Boolean for ShefferOrthoLattStr ;
coherence
 for b1 being non empty ShefferOrthoLattStr st b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 & b1 is properly_defined holds
( b1 is Boolean & b1 is Lattice-like ) by SHEFFER1:37;
cluster non empty Lattice-like Boolean well-complemented properly_defined  ->  non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for ShefferOrthoLattStr ;
coherence
 for b1 being non empty ShefferOrthoLattStr st b1 is Boolean & b1 is Lattice-like & b1 is well-complemented & b1 is properly_defined holds
( b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 ) by SHEFFER1:26, SHEFFER1:27, SHEFFER1:28;
end;

begin

theorem Th70: :: SHEFFER2:70
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, w being Element of L holds w | ((x | x) | x) = w | w
proofend;

theorem Th71: :: SHEFFER2:71
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, x being Element of L holds x = (x | x) | (p | (p | p))
proofend;

theorem Th72: :: SHEFFER2:72
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds (w | w) | (w | (y | (y | y))) = w
proofend;

theorem Th73: :: SHEFFER2:73
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, p, y, w being Element of L holds ((w | (y | (y | y))) | p) | ((q | q) | p) = (p | (w | q)) | (p | (w | q))
proofend;

theorem Th74: :: SHEFFER2:74
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, p, x being Element of L holds (x | p) | ((q | q) | p) = (p | ((x | x) | q)) | (p | ((x | x) | q))
proofend;

theorem Th75: :: SHEFFER2:75
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p, y, q being Element of L holds ((w | w) | p) | ((q | (y | (y | y))) | p) = (p | (w | q)) | (p | (w | q))
proofend;

theorem Th76: :: SHEFFER2:76
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, x being Element of L holds x = (x | x) | ((p | p) | p)
proofend;

theorem Th77: :: SHEFFER2:77
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds (w | w) | (w | ((y | y) | y)) = w
proofend;

theorem Th78: :: SHEFFER2:78
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds (w | ((y | y) | y)) | (w | w) = w
proofend;

theorem Th79: :: SHEFFER2:79
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, y, w being Element of L holds (w | ((y | y) | y)) | (p | (p | p)) = w
proofend;

theorem Th80: :: SHEFFER2:80
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, x, y being Element of L holds ((y | (x | x)) | (y | (x | x))) | (p | (p | p)) = (x | x) | y
proofend;

theorem Th81: :: SHEFFER2:81
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y being Element of L holds y | (x | x) = (x | x) | y
proofend;

theorem Th82: :: SHEFFER2:82
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds w | y = ((y | y) | (y | y)) | w
proofend;

theorem Th83: :: SHEFFER2:83
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds w | y = y | w
proofend;

theorem Th84: :: SHEFFER2:84
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, p being Element of L holds (p | x) | (p | ((x | x) | (x | x))) = (((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p)
proofend;

theorem Th85: :: SHEFFER2:85
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, p being Element of L holds (p | x) | (p | x) = (((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p)
proofend;

theorem Th86: :: SHEFFER2:86
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, p being Element of L holds (p | x) | (p | x) = (x | p) | (((x | x) | (x | x)) | p)
proofend;

theorem Th87: :: SHEFFER2:87
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, p being Element of L holds (p | x) | (p | x) = (x | p) | (x | p)
proofend;

theorem Th88: :: SHEFFER2:88
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, q, w being Element of L holds ((w | q) | ((y | y) | y)) | ((w | q) | (w | q)) = ((w | w) | (w | q)) | ((q | q) | (w | q))
proofend;

theorem Th89: :: SHEFFER2:89
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, w being Element of L holds w | q = ((w | w) | (w | q)) | ((q | q) | (w | q))
proofend;

theorem Th90: :: SHEFFER2:90
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, p being Element of L holds (p | p) | (p | ((q | q) | q)) = (((q | q) | (q | q)) | p) | ((q | q) | p)
proofend;

theorem Th91: :: SHEFFER2:91
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, q being Element of L holds p = (((q | q) | (q | q)) | p) | ((q | q) | p)
proofend;

theorem Th92: :: SHEFFER2:92
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, q being Element of L holds p = (q | p) | ((q | q) | p)
proofend;

theorem Th93: :: SHEFFER2:93
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, w, x being Element of L 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)))
proofend;

theorem Th94: :: SHEFFER2:94
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, w, x being Element of L holds (((x | x) | w) | ((z | z) | w)) | ((w | (x | z)) | (w | (x | z))) = w | (x | z)
proofend;

theorem Th95: :: SHEFFER2:95
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p being Element of L holds (p | p) | (p | (w | (w | w))) = ((w | w) | p) | (((w | w) | (w | w)) | p)
proofend;

theorem Th96: :: SHEFFER2:96
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds p = ((w | w) | p) | (((w | w) | (w | w)) | p)
proofend;

theorem Th97: :: SHEFFER2:97
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds p = ((w | w) | p) | (w | p)
proofend;

theorem Th98: :: SHEFFER2:98
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, q, x being Element of L 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))
proofend;

theorem Th99: :: SHEFFER2:99
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, z, x being Element of L holds q | (x | z) = (((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q))
proofend;

theorem Th100: :: SHEFFER2:100
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, z, x being Element of L holds q | (x | z) = (z | ((x | x) | q)) | ((q | q) | ((x | x) | q))
proofend;

theorem Th101: :: SHEFFER2:101
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, y being Element of L holds w | w = ((y | y) | y) | w
proofend;

theorem Th102: :: SHEFFER2:102
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p being Element of L holds (p | w) | ((w | w) | p) = p
proofend;

theorem Th103: :: SHEFFER2:103
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds (w | w) | ((w | w) | ((y | y) | y)) = (y | y) | y
proofend;

theorem Th104: :: SHEFFER2:104
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds (w | w) | w = (y | y) | y
proofend;

theorem Th105: :: SHEFFER2:105
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds (w | p) | (p | (w | w)) = p
proofend;

theorem Th106: :: SHEFFER2:106
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p being Element of L holds (p | (w | w)) | (w | p) = p
proofend;

theorem Th107: :: SHEFFER2:107
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds (w | p) | (w | (p | p)) = w
proofend;

theorem Th108: :: SHEFFER2:108
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y being Element of L holds y | (((y | (x | x)) | (y | (x | x))) | (x | y)) = x | y
proofend;

theorem Th109: :: SHEFFER2:109
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds (w | (p | p)) | (w | p) = w
proofend;

theorem Th110: :: SHEFFER2:110
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w, q, y being Element of L holds (((y | y) | y) | q) | ((w | w) | q) = (q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w))
proofend;

theorem Th111: :: SHEFFER2:111
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, w, p being Element of L holds (q | q) | ((w | w) | q) = (q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w))
proofend;

theorem Th112: :: SHEFFER2:112
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, y, p being Element of L holds (w | p) | (w | (p | (y | (y | y)))) = w
proofend;

theorem Th113: :: SHEFFER2:113
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, y, p being Element of L holds (w | (p | (y | (y | y)))) | (w | p) = w
proofend;

theorem Th114: :: SHEFFER2:114
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, p, y being Element of L holds (((y | y) | y) | p) | ((q | q) | p) = (p | ((p | p) | q)) | (p | ((p | p) | q))
proofend;

theorem Th115: :: SHEFFER2:115
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, z, x being Element of L holds ((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q)) = (((z | z) | (z | z)) | (x | q)) | ((q | q) | (x | q))
proofend;

theorem Th116: :: SHEFFER2:116
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, z, x being Element of L holds ((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q)) = (z | (x | q)) | ((q | q) | (x | q))
proofend;

theorem Th117: :: SHEFFER2:117
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, q, z being Element of L holds ((w | w) | ((z | z) | q)) | ((q | ((q | q) | z)) | (q | ((q | q) | z))) = (((z | z) | q) | (w | q)) | (((z | z) | q) | (w | q))
proofend;

theorem Th118: :: SHEFFER2:118
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, p, x being Element of L holds ((p | (x | p)) | (p | (x | p))) | (q | (q | q)) = (x | x) | p
proofend;

theorem Th119: :: SHEFFER2:119
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, x being Element of L holds p | (x | p) = (x | x) | p
proofend;

theorem Th120: :: SHEFFER2:120
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, y being Element of L holds (y | p) | ((y | y) | p) = (p | p) | (y | p)
proofend;

theorem Th121: :: SHEFFER2:121
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y being Element of L holds x = (x | x) | (y | x)
proofend;

theorem Th122: :: SHEFFER2:122
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y being Element of L holds (y | x) | x = ((x | (y | y)) | (x | (y | y))) | (y | x)
proofend;

theorem Th123: :: SHEFFER2:123
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, z, y being Element of L holds ((x | ((y | y) | z)) | (x | ((y | y) | z))) | ((y | x) | ((z | z) | x)) = (z | (y | x)) | x
proofend;

theorem Th124: :: SHEFFER2:124
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y, z being Element of L holds (x | (((z | (z | z)) | (z | (z | z))) | y)) | (x | (((z | (z | z)) | (z | (z | z))) | y)) = x
proofend;

theorem Th125: :: SHEFFER2:125
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, z, y being Element of L holds (x | ((y | y) | z)) | z = z | (y | x)
proofend;

theorem Th126: :: SHEFFER2:126
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y being Element of L holds x | ((y | x) | x) = y | x
proofend;

theorem Th127: :: SHEFFER2:127
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, y, x being Element of L holds y = (((x | x) | x) | y) | ((z | z) | y)
proofend;

theorem Th128: :: SHEFFER2:128
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, y being Element of L holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y
proofend;

theorem Th129: :: SHEFFER2:129
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, z, y being Element of L holds (((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z)) = ((x | x) | ((y | y) | z)) | z
proofend;

theorem Th130: :: SHEFFER2:130
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, z, y being Element of L holds (((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z)) = z | (y | (x | x))
proofend;

theorem Th131: :: SHEFFER2:131
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, x being Element of L holds ((x | y) | (x | y)) | x = x | y
proofend;

theorem Th132: :: SHEFFER2:132
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds (w | w) | (w | p) = w
proofend;

theorem Th133: :: SHEFFER2:133
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p being Element of L holds (p | w) | (w | w) = w
proofend;

theorem Th134: :: SHEFFER2:134
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, y, w being Element of L holds (w | (y | (y | y))) | (w | p) = w
proofend;

theorem Th135: :: SHEFFER2:135
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds (w | p) | (w | w) = w
proofend;

theorem Th136: :: SHEFFER2:136
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, p, w being Element of L holds (w | p) | (w | (y | (y | y))) = w
proofend;

theorem Th137: :: SHEFFER2:137
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, q, w, y, x being Element of L 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)))
proofend;

theorem Th138: :: SHEFFER2:138
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, w, y, x being Element of L holds (((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q))) = w | (((x | q) | (x | q)) | (w | (x | q)))
proofend;

theorem Th139: :: SHEFFER2:139
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, w, y, x being Element of L holds (((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q))) = w | (x | q)
proofend;

theorem Th140: :: SHEFFER2:140
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, p, q, y, x being Element of L 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))
proofend;

theorem Th141: :: SHEFFER2:141
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, p, q, y, x being Element of L holds q | (x | z) = (((z | z) | (p | (p | p))) | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q))
proofend;

theorem Th142: :: SHEFFER2:142
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, q, y, x being Element of L holds q | (x | z) = (z | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q))
proofend;

theorem Th143: :: SHEFFER2:143
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for v, p, y, x being Element of L holds p | (x | v) = (v | ((x | (y | (y | y))) | p)) | p
proofend;

theorem Th144: :: SHEFFER2:144
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w, z, v, x being Element of L holds (w | (z | (x | v))) | (((x | (y | (y | y))) | z) | ((v | v) | z)) = z | (x | v)
proofend;

theorem Th145: :: SHEFFER2:145
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, z, x being Element of L holds ((y | ((x | x) | z)) | (y | ((x | x) | z))) | ((x | y) | ((z | z) | y)) = y | ((x | x) | z)
proofend;

theorem Th146: :: SHEFFER2:146
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, y, x being Element of L holds (z | (x | y)) | y = y | ((x | x) | z)
proofend;

theorem Th147: :: SHEFFER2:147
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, w, y, z being Element of L holds (((x | x) | w) | ((z | (y | (y | y))) | w)) | w = w | (x | z)
proofend;

theorem Th148: :: SHEFFER2:148
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, w, x being Element of L holds w | (z | ((x | x) | w)) = w | (x | z)
proofend;

theorem Th149: :: SHEFFER2:149
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, z, y, x being Element of L 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))
proofend;

theorem Th150: :: SHEFFER2:150
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, z, y, x being Element of L holds z | (x | p) = (((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z))
proofend;

theorem Th151: :: SHEFFER2:151
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, p, y, x being Element of L holds z | (x | p) = z | (p | ((x | (y | (y | y))) | (x | (y | (y | y)))))
proofend;

theorem Th152: :: SHEFFER2:152
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, p, x being Element of L holds z | (x | p) = z | (p | x)
proofend;

theorem Th153: :: SHEFFER2:153
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, q, p being Element of L holds (p | q) | w = w | (q | p)
proofend;

theorem Th154: :: SHEFFER2:154
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p, q being Element of L holds ((q | p) | w) | q = q | ((p | p) | w)
proofend;

theorem Th155: :: SHEFFER2:155
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, w, y, x being Element of L holds w | x = w | ((x | z) | (((x | (y | (y | y))) | (x | (y | (y | y)))) | w))
proofend;

theorem Th156: :: SHEFFER2:156
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, z, x being Element of L holds w | x = w | ((x | z) | (x | w))
proofend;

theorem Th157: :: SHEFFER2:157
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, x, z, y being Element of L holds (x | y) | (((x | (y | (z | (z | z)))) | q) | x) = (x | y) | (x | (y | (z | (z | z))))
proofend;

theorem Th158: :: SHEFFER2:158
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, q, z, y being Element of L holds (x | y) | (x | (((y | (z | (z | z))) | (y | (z | (z | z)))) | q)) = (x | y) | (x | (y | (z | (z | z))))
proofend;

theorem Th159: :: SHEFFER2:159
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, x, q, y being Element of L holds (x | y) | (x | (y | q)) = (x | y) | (x | (y | (z | (z | z))))
proofend;

theorem Th160: :: SHEFFER2:160
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, q, y being Element of L holds (x | y) | (x | (y | q)) = x
proofend;

theorem Th161: :: SHEFFER2:161
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr holds L is satisfying_Sh_1
proofend;

registration
cluster non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3  ->  non empty satisfying_Sh_1 for ShefferStr ;
coherence
 for b1 being non empty ShefferStr st b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 holds
b1 is satisfying_Sh_1 by Th161;
cluster non empty satisfying_Sh_1  ->  non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for ShefferStr ;
coherence
 for b1 being non empty ShefferStr st b1 is satisfying_Sh_1 holds
( b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 ) by Th67, Th68, Th69;
end;

registration
cluster non empty properly_defined satisfying_Sh_1  ->  non empty Lattice-like Boolean for ShefferOrthoLattStr ;
coherence
 for b1 being non empty ShefferOrthoLattStr st b1 is satisfying_Sh_1 & b1 is properly_defined holds
( b1 is Boolean & b1 is Lattice-like ) ;
cluster non empty Lattice-like Boolean well-complemented properly_defined  ->  non empty satisfying_Sh_1 for ShefferOrthoLattStr ;
coherence
 for b1 being non empty ShefferOrthoLattStr st b1 is Boolean & b1 is Lattice-like & b1 is well-complemented & b1 is properly_defined holds
b1 is satisfying_Sh_1 ;
end;