:: SHEFFER2 semantic presentation

definition

let c₁ be non empty ShefferStr ;
attr a₁ is satisfying_Sh_1 means :Def1: :: SHEFFER2:def 1
for b₁, b₂, b₃ being Element of a₁ holds (b₁ | ((b₂ | b₁) | b₁)) | (b₂ | (b₃ | b₁)) = b₂;

end;

:: deftheorem Def1 defines satisfying_Sh_1 SHEFFER2:def 1 :

registration

cluster non empty trivial -> non empty satisfying_Sh_1 ShefferStr ;
coherence

proof end;

end;

registration

cluster non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 ShefferStr ;
existence

proof end;

end;

theorem Th1: :: SHEFFER2:1

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds ((b₂ | (b₃ | b₄)) | (b₂ | (b₂ | (b₃ | b₄)))) | ((b₄ | ((b₂ | b₄) | b₄)) | (b₅ | (b₂ | (b₃ | b₄)))) = b₄ | ((b₂ | b₄) | b₄)

proof end;

theorem Th2: :: SHEFFER2:2

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ | b₃) | (((b₃ | ((b₄ | b₃) | b₃)) | (b₂ | b₃)) | (b₂ | b₃))) | b₄ = b₃ | ((b₄ | b₃) | b₃)

proof end;

theorem Th3: :: SHEFFER2:3

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | ((b₃ | b₂) | b₂)) | (b₃ | (b₄ | ((b₂ | b₄) | b₄))) = b₃

proof end;

theorem Th4: :: SHEFFER2:4

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | ((b₂ | ((b₂ | b₂) | b₂)) | (b₃ | (b₂ | ((b₂ | b₂) | b₂)))) = b₂ | ((b₂ | b₂) | b₂)

proof end;

theorem Th5: :: SHEFFER2:5

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂ being Element of b₁ holds b₂ | ((b₂ | b₂) | b₂) = b₂ | b₂

proof end;

theorem Th6: :: SHEFFER2:6

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂ being Element of b₁ holds (b₂ | ((b₂ | b₂) | b₂)) | (b₂ | b₂) = b₂

proof end;

theorem Th7: :: SHEFFER2:7

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₂ | b₂) | (b₂ | (b₃ | b₂)) = b₂

proof end;

theorem Th8: :: SHEFFER2:8

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₂ | (((b₃ | b₃) | b₂) | b₂)) | b₃ = b₃ | b₃

proof end;

theorem Th9: :: SHEFFER2:9

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds ((b₂ | b₃) | (((b₂ | b₃) | (b₂ | b₃)) | (b₂ | b₃))) | ((b₂ | b₃) | (b₂ | b₃)) = b₃ | ((((b₂ | b₃) | (b₂ | b₃)) | b₃) | b₃)

proof end;

theorem Th10: :: SHEFFER2:10

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | ((((b₃ | b₂) | (b₃ | b₂)) | b₂) | b₂) = b₃ | b₂

proof end;

theorem Th11: :: SHEFFER2:11

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₂ | b₂) | (b₃ | b₂) = b₂

proof end;

theorem Th12: :: SHEFFER2:12

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | (b₃ | (b₂ | b₂)) = b₂ | b₂

proof end;

theorem Th13: :: SHEFFER2:13

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds ((b₂ | b₃) | (b₂ | b₃)) | b₃ = b₂ | b₃

proof end;

theorem Th14: :: SHEFFER2:14

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | ((b₃ | b₂) | b₂) = b₃ | b₂

proof end;

theorem Th15: :: SHEFFER2:15

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | b₃) | (b₂ | (b₄ | b₃)) = b₂

proof end;

theorem Th16: :: SHEFFER2:16

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | b₄)) | (b₂ | b₄) = b₂

proof end;

theorem Th17: :: SHEFFER2:17

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | ((b₂ | b₃) | (b₄ | b₃)) = b₂ | b₃

proof end;

theorem Th18: :: SHEFFER2:18

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ | (b₃ | b₄)) | b₄) | b₂ = b₂ | (b₃ | b₄)

proof end;

theorem Th19: :: SHEFFER2:19

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | ((b₃ | b₂) | b₂) = b₂ | b₃

proof end;

theorem Th20: :: SHEFFER2:20

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | b₃ = b₃ | b₂

proof end;

theorem Th21: :: SHEFFER2:21

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₂ | b₃) | (b₂ | b₂) = b₂

proof end;

theorem Th22: :: SHEFFER2:22

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | b₃) | (b₃ | (b₄ | b₂)) = b₃

proof end;

theorem Th23: :: SHEFFER2:23

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | b₄)) | (b₄ | b₂) = b₂

proof end;

theorem Th24: :: SHEFFER2:24

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | b₃) | (b₃ | (b₂ | b₄)) = b₃

proof end;

theorem Th25: :: SHEFFER2:25

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | b₄)) | (b₃ | b₂) = b₂

proof end;

theorem Th26: :: SHEFFER2:26

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ | b₃) | (b₂ | b₄)) | b₄ = b₂ | b₄

proof end;

theorem Th27: :: SHEFFER2:27

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₃ | (b₂ | (b₃ | b₄))) = b₂ | (b₃ | b₄)

proof end;

theorem Th28: :: SHEFFER2:28

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | (b₂ | b₄))) | b₃ = b₃ | (b₂ | b₄)

proof end;

theorem Th29: :: SHEFFER2:29

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds (b₂ | (b₃ | b₄)) | (b₂ | (b₅ | (b₃ | b₂))) = (b₂ | (b₃ | b₄)) | (b₃ | b₂)

proof end;

theorem Th30: :: SHEFFER2:30

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | (b₂ | b₄))) | b₃ = b₃ | (b₄ | b₂)

proof end;

theorem Th31: :: SHEFFER2:31

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds (b₂ | (b₃ | b₄)) | (b₂ | (b₅ | (b₃ | b₂))) = b₂

proof end;

theorem Th32: :: SHEFFER2:32

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | (b₃ | (b₂ | b₃)) = b₂ | b₂

proof end;

theorem Th33: :: SHEFFER2:33

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₃ | b₄) = b₂ | (b₄ | b₃)

proof end;

theorem Th34: :: SHEFFER2:34

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₃ | (b₂ | (b₄ | (b₃ | b₂)))) = b₂ | b₂

proof end;

theorem Th35: :: SHEFFER2:35

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | b₄)) | ((b₃ | b₂) | b₂) = (b₂ | (b₃ | b₄)) | (b₂ | (b₃ | b₄))

proof end;

theorem Th36: :: SHEFFER2:36

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₂ | (b₃ | b₂)) | b₃ = b₃ | b₃

proof end;

theorem Th37: :: SHEFFER2:37

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | b₃) | b₄ = b₄ | (b₃ | b₂)

proof end;

theorem Th38: :: SHEFFER2:38

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₃ | (b₄ | (b₂ | b₃))) = b₂ | (b₃ | b₃)

proof end;

theorem Th39: :: SHEFFER2:39

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ | b₃) | b₃) | (b₃ | (b₄ | b₂)) = (b₃ | (b₄ | b₂)) | (b₃ | (b₄ | b₂))

proof end;

theorem Th40: :: SHEFFER2:40

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds (b₂ | b₃) | (b₄ | b₅) = (b₅ | b₄) | (b₃ | b₂)

proof end;

theorem Th41: :: SHEFFER2:41

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₃ | ((b₃ | b₂) | b₄)) = b₂ | (b₃ | b₃)

proof end;

theorem Th42: :: SHEFFER2:42

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | (b₃ | b₂) = b₂ | (b₃ | b₃)

proof end;

theorem Th43: :: SHEFFER2:43

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₂ | b₃) | b₃ = b₃ | (b₂ | b₂)

proof end;

theorem Th44: :: SHEFFER2:44

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | (b₃ | b₃) = b₂ | (b₂ | b₃)

proof end;

theorem Th45: :: SHEFFER2:45

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | b₃)) | (b₂ | (b₄ | b₃)) = (b₂ | (b₄ | b₃)) | (b₂ | (b₄ | b₃))

proof end;

theorem Th46: :: SHEFFER2:46

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | b₄)) | (b₂ | (b₃ | b₃)) = (b₂ | (b₃ | b₄)) | (b₂ | (b₃ | b₄))

proof end;

theorem Th47: :: SHEFFER2:47

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | ((b₃ | b₃) | (b₄ | (b₂ | (b₂ | b₃)))) = b₂ | ((b₃ | b₃) | (b₃ | b₃))

proof end;

theorem Th48: :: SHEFFER2:48

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ | (b₃ | b₄)) | (b₂ | (b₃ | b₄))) | (b₃ | b₃) = b₂ | (b₃ | b₃)

proof end;

theorem Th49: :: SHEFFER2:49

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | ((b₃ | b₃) | (b₄ | (b₂ | (b₂ | b₃)))) = b₂ | b₃

proof end;

theorem Th50: :: SHEFFER2:50

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (((b₂ | b₃) | (b₂ | b₃)) | ((b₄ | ((b₂ | b₃) | b₄)) | (b₂ | b₃))) | (b₂ | b₂) = (b₄ | ((b₂ | b₃) | b₄)) | (b₂ | b₂)

proof end;

theorem Th51: :: SHEFFER2:51

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | ((b₃ | b₄) | b₂)) | (b₃ | b₃) = (b₃ | b₄) | (b₃ | b₃)

proof end;

theorem Th52: :: SHEFFER2:52

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | ((b₃ | b₄) | b₂)) | (b₃ | b₃) = b₃

proof end;

theorem Th53: :: SHEFFER2:53

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | ((b₃ | ((b₂ | b₄) | b₃)) | b₂) = b₃ | ((b₂ | b₄) | b₃)

proof end;

theorem Th54: :: SHEFFER2:54

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | ((b₃ | (b₃ | (b₄ | b₂))) | b₂) = b₃ | ((b₂ | (b₃ | (b₂ | b₄))) | b₃)

proof end;

theorem Th55: :: SHEFFER2:55

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | ((b₃ | (b₃ | (b₄ | b₂))) | b₂) = b₃ | (b₃ | (b₄ | b₂))

proof end;

theorem Th56: :: SHEFFER2:56

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds b₂ | (b₃ | (b₄ | (b₄ | (b₅ | (b₃ | b₂))))) = b₂ | (b₃ | b₃)

proof end;

theorem Th57: :: SHEFFER2:57

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₃ | (b₃ | (b₄ | (b₂ | b₃)))) = b₂ | (b₃ | (b₂ | b₂))

proof end;

theorem Th58: :: SHEFFER2:58

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₃ | (b₃ | (b₄ | (b₂ | b₃)))) = b₂ | b₂

proof end;

theorem Th59: :: SHEFFER2:59

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | (b₃ | (b₃ | b₃)) = b₂ | b₂

proof end;

theorem Th60: :: SHEFFER2:60

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (((b₃ | (b₄ | b₂)) | (b₃ | (b₄ | b₂))) | (b₄ | b₄)) = b₂ | (b₃ | (b₄ | b₂))

proof end;

theorem Th61: :: SHEFFER2:61

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₃ | (b₄ | b₄)) = b₂ | (b₃ | (b₄ | b₂))

proof end;

theorem Th62: :: SHEFFER2:62

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₃ | ((b₄ | b₄) | b₂)) = b₂ | (b₃ | b₄)

proof end;

theorem Th63: :: SHEFFER2:63

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | b₃)) | (b₂ | (b₄ | ((b₃ | b₃) | b₂))) = (b₂ | (b₄ | b₃)) | (b₂ | (b₄ | b₃))

proof end;

theorem Th64: :: SHEFFER2:64

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | b₃)) | (b₂ | (b₄ | (b₂ | (b₃ | b₃)))) = (b₂ | (b₄ | b₃)) | (b₂ | (b₄ | b₃))

proof end;

theorem Th65: :: SHEFFER2:65

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | b₃)) | (b₂ | (b₄ | b₄)) = (b₂ | (b₄ | b₃)) | (b₂ | (b₄ | b₃))

proof end;

theorem Th66: :: SHEFFER2:66

for b₁ being non empty satisfying_Sh_1 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ | b₂) | b₃) | ((b₄ | b₄) | b₃) = (b₃ | (b₂ | b₄)) | (b₃ | (b₂ | b₄))

proof end;

theorem Th67: :: SHEFFER2:67

for b₁ being non empty ShefferStr st b₁ is satisfying_Sh_1 holds
b₁ is satisfying_Sheffer_1

proof end;

theorem Th68: :: SHEFFER2:68

for b₁ being non empty ShefferStr st b₁ is satisfying_Sh_1 holds
b₁ is satisfying_Sheffer_2

proof end;

theorem Th69: :: SHEFFER2:69

for b₁ being non empty ShefferStr st b₁ is satisfying_Sh_1 holds
b₁ 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

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 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 by SHEFFER1:27, SHEFFER1:28, SHEFFER1:29;

end;

theorem Th70: :: SHEFFER2:70

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₃ | ((b₂ | b₂) | b₂) = b₃ | b₃

proof end;

theorem Th71: :: SHEFFER2:71

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₃ = (b₃ | b₃) | (b₂ | (b₂ | b₂))

proof end;

theorem Th72: :: SHEFFER2:72

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₃) | (b₃ | (b₂ | (b₂ | b₂))) = b₃

proof end;

theorem Th73: :: SHEFFER2:73

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds ((b₅ | (b₄ | (b₄ | b₄))) | b₃) | ((b₂ | b₂) | b₃) = (b₃ | (b₅ | b₂)) | (b₃ | (b₅ | b₂))

proof end;

theorem Th74: :: SHEFFER2:74

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₄ | b₃) | ((b₂ | b₂) | b₃) = (b₃ | ((b₄ | b₄) | b₂)) | (b₃ | ((b₄ | b₄) | b₂))

proof end;

theorem Th75: :: SHEFFER2:75

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds ((b₂ | b₂) | b₃) | ((b₅ | (b₄ | (b₄ | b₄))) | b₃) = (b₃ | (b₂ | b₅)) | (b₃ | (b₂ | b₅))

proof end;

theorem Th76: :: SHEFFER2:76

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₃ = (b₃ | b₃) | ((b₂ | b₂) | b₂)

proof end;

theorem Th77: :: SHEFFER2:77

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₃) | (b₃ | ((b₂ | b₂) | b₂)) = b₃

proof end;

theorem Th78: :: SHEFFER2:78

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | ((b₂ | b₂) | b₂)) | (b₃ | b₃) = b₃

proof end;

theorem Th79: :: SHEFFER2:79

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₄ | ((b₃ | b₃) | b₃)) | (b₂ | (b₂ | b₂)) = b₄

proof end;

theorem Th80: :: SHEFFER2:80

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₄ | (b₃ | b₃)) | (b₄ | (b₃ | b₃))) | (b₂ | (b₂ | b₂)) = (b₃ | b₃) | b₄

proof end;

theorem Th81: :: SHEFFER2:81

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₃ | (b₂ | b₂) = (b₂ | b₂) | b₃

proof end;

theorem Th82: :: SHEFFER2:82

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₃ | b₂ = ((b₂ | b₂) | (b₂ | b₂)) | b₃

proof end;

theorem Th83: :: SHEFFER2:83

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₃ | b₂ = b₂ | b₃

proof end;

theorem Th84: :: SHEFFER2:84

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | (b₃ | ((b₂ | b₂) | (b₂ | b₂))) = (((b₂ | b₂) | (b₂ | b₂)) | b₃) | (((b₂ | b₂) | (b₂ | b₂)) | b₃)

proof end;

theorem Th85: :: SHEFFER2:85

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | (b₃ | b₂) = (((b₂ | b₂) | (b₂ | b₂)) | b₃) | (((b₂ | b₂) | (b₂ | b₂)) | b₃)

proof end;

theorem Th86: :: SHEFFER2:86

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | (b₃ | b₂) = (b₂ | b₃) | (((b₂ | b₂) | (b₂ | b₂)) | b₃)

proof end;

theorem Th87: :: SHEFFER2:87

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | (b₃ | b₂) = (b₂ | b₃) | (b₂ | b₃)

proof end;

theorem Th88: :: SHEFFER2:88

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₄ | b₃) | ((b₂ | b₂) | b₂)) | ((b₄ | b₃) | (b₄ | b₃)) = ((b₄ | b₄) | (b₄ | b₃)) | ((b₃ | b₃) | (b₄ | b₃))

proof end;

theorem Th89: :: SHEFFER2:89

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₃ | b₂ = ((b₃ | b₃) | (b₃ | b₂)) | ((b₂ | b₂) | (b₃ | b₂))

proof end;

theorem Th90: :: SHEFFER2:90

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₃) | (b₃ | ((b₂ | b₂) | b₂)) = (((b₂ | b₂) | (b₂ | b₂)) | b₃) | ((b₂ | b₂) | b₃)

proof end;

theorem Th91: :: SHEFFER2:91

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ = (((b₃ | b₃) | (b₃ | b₃)) | b₂) | ((b₃ | b₃) | b₂)

proof end;

theorem Th92: :: SHEFFER2:92

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ = (b₃ | b₂) | ((b₃ | b₃) | b₂)

proof end;

theorem Th93: :: SHEFFER2:93

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (((b₄ | b₄) | b₃) | ((b₂ | b₂) | b₃)) | ((b₃ | (b₄ | b₂)) | (b₃ | (b₄ | b₂))) = ((b₃ | b₃) | (b₃ | (b₄ | b₂))) | (((b₄ | b₂) | (b₄ | b₂)) | (b₃ | (b₄ | b₂)))

proof end;

theorem Th94: :: SHEFFER2:94

proof end;

theorem Th95: :: SHEFFER2:95

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₃) | (b₃ | (b₂ | (b₂ | b₂))) = ((b₂ | b₂) | b₃) | (((b₂ | b₂) | (b₂ | b₂)) | b₃)

proof end;

theorem Th96: :: SHEFFER2:96

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ = ((b₃ | b₃) | b₂) | (((b₃ | b₃) | (b₃ | b₃)) | b₂)

proof end;

theorem Th97: :: SHEFFER2:97

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ = ((b₃ | b₃) | b₂) | (b₃ | b₂)

proof end;

theorem Th98: :: SHEFFER2:98

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (((b₄ | b₄) | b₃) | ((b₂ | b₂) | b₃)) | ((b₃ | (b₄ | b₂)) | (b₃ | (b₄ | b₂))) = (((b₂ | b₂) | (b₂ | b₂)) | ((b₄ | b₄) | b₃)) | ((b₃ | b₃) | ((b₄ | b₄) | b₃))

proof end;

theorem Th99: :: SHEFFER2:99

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₄ | b₃) = (((b₃ | b₃) | (b₃ | b₃)) | ((b₄ | b₄) | b₂)) | ((b₂ | b₂) | ((b₄ | b₄) | b₂))

proof end;

theorem Th100: :: SHEFFER2:100

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₄ | b₃) = (b₃ | ((b₄ | b₄) | b₂)) | ((b₂ | b₂) | ((b₄ | b₄) | b₂))

proof end;

theorem Th101: :: SHEFFER2:101

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | b₂ = ((b₃ | b₃) | b₃) | b₂

proof end;

theorem Th102: :: SHEFFER2:102

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | ((b₂ | b₂) | b₃) = b₃

proof end;

theorem Th103: :: SHEFFER2:103

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₃) | ((b₃ | b₃) | ((b₂ | b₂) | b₂)) = (b₂ | b₂) | b₂

proof end;

theorem Th104: :: SHEFFER2:104

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₃) | b₃ = (b₂ | b₂) | b₂

proof end;

theorem Th105: :: SHEFFER2:105

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | (b₂ | (b₃ | b₃)) = b₂

proof end;

theorem Th106: :: SHEFFER2:106

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | (b₂ | b₂)) | (b₂ | b₃) = b₃

proof end;

theorem Th107: :: SHEFFER2:107

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | (b₃ | (b₂ | b₂)) = b₃

proof end;

theorem Th108: :: SHEFFER2:108

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₃ | (((b₃ | (b₂ | b₂)) | (b₃ | (b₂ | b₂))) | (b₂ | b₃)) = b₂ | b₃

proof end;

theorem Th109: :: SHEFFER2:109

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | (b₂ | b₂)) | (b₃ | b₂) = b₃

proof end;

theorem Th110: :: SHEFFER2:110

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds (((b₅ | b₅) | b₅) | b₄) | ((b₃ | b₃) | b₄) = (b₄ | (((b₂ | (b₂ | b₂)) | (b₂ | (b₂ | b₂))) | b₃)) | (b₄ | (((b₂ | (b₂ | b₂)) | (b₂ | (b₂ | b₂))) | b₃))

proof end;

theorem Th111: :: SHEFFER2:111

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | b₂) | ((b₃ | b₃) | b₂) = (b₂ | (((b₄ | (b₄ | b₄)) | (b₄ | (b₄ | b₄))) | b₃)) | (b₂ | (((b₄ | (b₄ | b₄)) | (b₄ | (b₄ | b₄))) | b₃))

proof end;

theorem Th112: :: SHEFFER2:112

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | b₄) | (b₂ | (b₄ | (b₃ | (b₃ | b₃)))) = b₂

proof end;

theorem Th113: :: SHEFFER2:113

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₄ | (b₃ | (b₃ | b₃)))) | (b₂ | b₄) = b₂

proof end;

theorem Th114: :: SHEFFER2:114

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (((b₄ | b₄) | b₄) | b₃) | ((b₂ | b₂) | b₃) = (b₃ | ((b₃ | b₃) | b₂)) | (b₃ | ((b₃ | b₃) | b₂))

proof end;

theorem Th115: :: SHEFFER2:115

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ | ((b₄ | b₄) | b₃)) | (b₂ | ((b₄ | b₄) | b₃))) | ((b₄ | b₂) | ((b₃ | b₃) | b₂)) = (((b₃ | b₃) | (b₃ | b₃)) | (b₄ | b₂)) | ((b₂ | b₂) | (b₄ | b₂))

proof end;

theorem Th116: :: SHEFFER2:116

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ | ((b₄ | b₄) | b₃)) | (b₂ | ((b₄ | b₄) | b₃))) | ((b₄ | b₂) | ((b₃ | b₃) | b₂)) = (b₃ | (b₄ | b₂)) | ((b₂ | b₂) | (b₄ | b₂))

proof end;

theorem Th117: :: SHEFFER2:117

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ | b₂) | ((b₄ | b₄) | b₃)) | ((b₃ | ((b₃ | b₃) | b₄)) | (b₃ | ((b₃ | b₃) | b₄))) = (((b₄ | b₄) | b₃) | (b₂ | b₃)) | (((b₄ | b₄) | b₃) | (b₂ | b₃))

proof end;

theorem Th118: :: SHEFFER2:118

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₃ | (b₄ | b₃)) | (b₃ | (b₄ | b₃))) | (b₂ | (b₂ | b₂)) = (b₄ | b₄) | b₃

proof end;

theorem Th119: :: SHEFFER2:119

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | (b₃ | b₂) = (b₃ | b₃) | b₂

proof end;

theorem Th120: :: SHEFFER2:120

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | ((b₃ | b₃) | b₂) = (b₂ | b₂) | (b₃ | b₂)

proof end;

theorem Th121: :: SHEFFER2:121

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ = (b₂ | b₂) | (b₃ | b₂)

proof end;

theorem Th122: :: SHEFFER2:122

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | b₂ = ((b₂ | (b₃ | b₃)) | (b₂ | (b₃ | b₃))) | (b₃ | b₂)

proof end;

theorem Th123: :: SHEFFER2:123

proof end;

theorem Th124: :: SHEFFER2:124

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (((b₄ | (b₄ | b₄)) | (b₄ | (b₄ | b₄))) | b₃)) | (b₂ | (((b₄ | (b₄ | b₄)) | (b₄ | (b₄ | b₄))) | b₃)) = b₂

proof end;

theorem Th125: :: SHEFFER2:125

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | ((b₄ | b₄) | b₃)) | b₃ = b₃ | (b₄ | b₂)

proof end;

theorem Th126: :: SHEFFER2:126

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds b₂ | ((b₃ | b₂) | b₂) = b₃ | b₂

proof end;

theorem Th127: :: SHEFFER2:127

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₃ = (((b₄ | b₄) | b₄) | b₃) | ((b₂ | b₂) | b₃)

proof end;

theorem Th128: :: SHEFFER2:128

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | ((b₃ | b₃) | b₂)) | (b₃ | ((b₃ | b₃) | b₂)) = b₃

proof end;

theorem Th129: :: SHEFFER2:129

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (((b₄ | b₄) | b₃) | (b₂ | b₃)) | (((b₄ | b₄) | b₃) | (b₂ | b₃)) = ((b₂ | b₂) | ((b₄ | b₄) | b₃)) | b₃

proof end;

theorem Th130: :: SHEFFER2:130

proof end;

theorem Th131: :: SHEFFER2:131

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds ((b₃ | b₂) | (b₃ | b₂)) | b₃ = b₃ | b₂

proof end;

theorem Th132: :: SHEFFER2:132

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₃) | (b₃ | b₂) = b₃

proof end;

theorem Th133: :: SHEFFER2:133

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | (b₂ | b₂) = b₂

proof end;

theorem Th134: :: SHEFFER2:134

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₄ | (b₃ | (b₃ | b₃))) | (b₄ | b₂) = b₄

proof end;

theorem Th135: :: SHEFFER2:135

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃ being Element of b₁ holds (b₃ | b₂) | (b₃ | b₃) = b₃

proof end;

theorem Th136: :: SHEFFER2:136

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₄ | b₃) | (b₄ | (b₂ | (b₂ | b₂))) = b₄

proof end;

theorem Th137: :: SHEFFER2:137

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds (((b₆ | (b₅ | (b₅ | b₅))) | b₄) | ((b₃ | b₃) | b₄)) | ((b₄ | (b₆ | b₃)) | (b₄ | (b₆ | b₃))) = ((b₄ | (b₂ | (b₂ | b₂))) | (b₄ | (b₆ | b₃))) | (((b₆ | b₃) | (b₆ | b₃)) | (b₄ | (b₆ | b₃)))

proof end;

theorem Th138: :: SHEFFER2:138

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds (((b₅ | (b₄ | (b₄ | b₄))) | b₃) | ((b₂ | b₂) | b₃)) | ((b₃ | (b₅ | b₂)) | (b₃ | (b₅ | b₂))) = b₃ | (((b₅ | b₂) | (b₅ | b₂)) | (b₃ | (b₅ | b₂)))

proof end;

theorem Th139: :: SHEFFER2:139

proof end;

theorem Th140: :: SHEFFER2:140

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds (((b₆ | (b₅ | (b₅ | b₅))) | b₄) | ((b₂ | b₂) | b₄)) | ((b₄ | (b₆ | b₂)) | (b₄ | (b₆ | b₂))) = (((b₂ | b₂) | (b₃ | (b₃ | b₃))) | ((b₆ | (b₅ | (b₅ | b₅))) | b₄)) | ((b₄ | b₄) | ((b₆ | (b₅ | (b₅ | b₅))) | b₄))

proof end;

theorem Th141: :: SHEFFER2:141

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds b₄ | (b₆ | b₂) = (((b₂ | b₂) | (b₃ | (b₃ | b₃))) | ((b₆ | (b₅ | (b₅ | b₅))) | b₄)) | ((b₄ | b₄) | ((b₆ | (b₅ | (b₅ | b₅))) | b₄))

proof end;

theorem Th142: :: SHEFFER2:142

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds b₃ | (b₅ | b₂) = (b₂ | ((b₅ | (b₄ | (b₄ | b₄))) | b₃)) | ((b₃ | b₃) | ((b₅ | (b₄ | (b₄ | b₄))) | b₃))

proof end;

theorem Th143: :: SHEFFER2:143

proof end;

theorem Th144: :: SHEFFER2:144

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds (b₃ | (b₄ | (b₆ | b₅))) | (((b₆ | (b₂ | (b₂ | b₂))) | b₄) | ((b₅ | b₅) | b₄)) = b₄ | (b₆ | b₅)

proof end;

theorem Th145: :: SHEFFER2:145

proof end;

theorem Th146: :: SHEFFER2:146

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₄ | b₃)) | b₃ = b₃ | ((b₄ | b₄) | b₂)

proof end;

theorem Th147: :: SHEFFER2:147

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds (((b₂ | b₂) | b₃) | ((b₅ | (b₄ | (b₄ | b₄))) | b₃)) | b₃ = b₃ | (b₂ | b₅)

proof end;

theorem Th148: :: SHEFFER2:148

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₃ | (b₂ | ((b₄ | b₄) | b₃)) = b₃ | (b₄ | b₂)

proof end;

theorem Th149: :: SHEFFER2:149

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds ((b₃ | (b₅ | b₂)) | (b₃ | (b₅ | b₂))) | (((b₅ | (b₄ | (b₄ | b₄))) | b₃) | ((b₂ | b₂) | b₃)) = (((b₂ | b₂) | b₃) | ((b₅ | (b₄ | (b₄ | b₄))) | b₃)) | (((b₂ | b₂) | b₃) | ((b₅ | (b₄ | (b₄ | b₄))) | b₃))

proof end;

theorem Th150: :: SHEFFER2:150

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds b₃ | (b₅ | b₂) = (((b₂ | b₂) | b₃) | ((b₅ | (b₄ | (b₄ | b₄))) | b₃)) | (((b₂ | b₂) | b₃) | ((b₅ | (b₄ | (b₄ | b₄))) | b₃))

proof end;

theorem Th151: :: SHEFFER2:151

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds b₂ | (b₅ | b₃) = b₂ | (b₃ | ((b₅ | (b₄ | (b₄ | b₄))) | (b₅ | (b₄ | (b₄ | b₄)))))

proof end;

theorem Th152: :: SHEFFER2:152

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | (b₄ | b₃) = b₂ | (b₃ | b₄)

proof end;

theorem Th153: :: SHEFFER2:153

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₄ | b₃) | b₂ = b₂ | (b₃ | b₄)

proof end;

theorem Th154: :: SHEFFER2:154

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₄ | b₃) | b₂) | b₄ = b₄ | ((b₃ | b₃) | b₂)

proof end;

theorem Th155: :: SHEFFER2:155

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds b₃ | b₅ = b₃ | ((b₅ | b₂) | (((b₅ | (b₄ | (b₄ | b₄))) | (b₅ | (b₄ | (b₄ | b₄)))) | b₃))

proof end;

theorem Th156: :: SHEFFER2:156

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ | b₄ = b₂ | ((b₄ | b₃) | (b₄ | b₂))

proof end;

theorem Th157: :: SHEFFER2:157

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds (b₃ | b₅) | (((b₃ | (b₅ | (b₄ | (b₄ | b₄)))) | b₂) | b₃) = (b₃ | b₅) | (b₃ | (b₅ | (b₄ | (b₄ | b₄))))

proof end;

theorem Th158: :: SHEFFER2:158

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds (b₂ | b₅) | (b₂ | (((b₅ | (b₄ | (b₄ | b₄))) | (b₅ | (b₄ | (b₄ | b₄)))) | b₃)) = (b₂ | b₅) | (b₂ | (b₅ | (b₄ | (b₄ | b₄))))

proof end;

theorem Th159: :: SHEFFER2:159

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds (b₃ | b₅) | (b₃ | (b₅ | b₄)) = (b₃ | b₅) | (b₃ | (b₅ | (b₂ | (b₂ | b₂))))

proof end;

theorem Th160: :: SHEFFER2:160

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | b₄) | (b₂ | (b₄ | b₃)) = b₂

proof end;

theorem Th161: :: SHEFFER2:161

for b₁ being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr holds b₁ 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 by Th161;
cluster non empty satisfying_Sh_1 -> non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ;
coherence by Th67, Th68, Th69;

end;

registration

cluster non empty properly_defined satisfying_Sh_1 -> non empty Lattice-like Boolean ShefferOrthoLattStr ;
coherence

proof end;

cluster non empty Lattice-like Boolean well-complemented properly_defined -> non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 ShefferOrthoLattStr ;
coherence

proof end;

end;