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

begin

definition

let L be non empty ShefferStr ;
attr L 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 ShefferStr ;
coherence
for b₁ being non empty ShefferStr st b₁ is trivial holds
b₁ is satisfying_Sh_1

proof end;

end;

registration

cluster non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 ShefferStr ;
existence
ex b₁ being non empty ShefferStr st
( b₁ is satisfying_Sh_1 & b₁ is satisfying_Sheffer_1 & b₁ is satisfying_Sheffer_2 & b₁ is satisfying_Sheffer_3 )

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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))

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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))

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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))

proof end;

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))

proof end;

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))

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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))

proof end;

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)

proof end;

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))

proof end;

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

proof end;

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

proof end;

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))

proof end;

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))

proof end;

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)

proof end;

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))

proof end;

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))

proof end;

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))

proof end;

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))

proof end;

theorem Th67: :: SHEFFER2:67

for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_1

proof end;

theorem Th68: :: SHEFFER2:68

for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_2

proof end;

theorem Th69: :: SHEFFER2:69

for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_3

proof end;

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 ShefferOrthoLattStr ;
existence
ex b₁ being non empty ShefferOrthoLattStr st
( b₁ is properly_defined & b₁ is Boolean & b₁ is well-complemented & b₁ is Lattice-like & b₁ is de_Morgan & b₁ is satisfying_Sheffer_1 & b₁ is satisfying_Sheffer_2 & b₁ is satisfying_Sheffer_3 & b₁ is satisfying_Sh_1 )

proof end;

end;

registration

cluster non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 -> non empty Lattice-like Boolean ShefferOrthoLattStr ;
coherence
for b₁ being non empty ShefferOrthoLattStr st b₁ is satisfying_Sheffer_1 & b₁ is satisfying_Sheffer_2 & b₁ is satisfying_Sheffer_3 & b₁ is properly_defined holds
( b₁ is Boolean & b₁ is Lattice-like ) by SHEFFER1:38;
cluster non empty Lattice-like Boolean well-complemented properly_defined -> non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ;
coherence
for b₁ being non empty ShefferOrthoLattStr st b₁ is Boolean & b₁ is Lattice-like & b₁ is well-complemented & b₁ is properly_defined holds
( b₁ is satisfying_Sheffer_1 & b₁ is satisfying_Sheffer_2 & b₁ is satisfying_Sheffer_3 ) by SHEFFER1:27, SHEFFER1:28, SHEFFER1:29;

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

proof end;

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))

proof end;

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

proof end;

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))

proof end;

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))

proof end;

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))

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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))

proof end;

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))

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)))

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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))

proof end;

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))

proof end;

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))

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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))

proof end;

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))

proof end;

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

proof end;

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

proof end;

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))

proof end;

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))

proof end;

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))

proof end;

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))

proof end;

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

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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))

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)))

proof end;

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)))

proof end;

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)

proof end;

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))

proof end;

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))

proof end;

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))

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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))

proof end;

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))

proof end;

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)))))

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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))

proof end;

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))

proof end;

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))))

proof end;

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))))

proof end;

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))))

proof end;

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

proof end;

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

proof end;

registration

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

end;

registration

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

end;