:: SHEFFER2 semantic presentation

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
proof
let L be non empty ShefferStr ; ::_thesis: ( L is trivial implies L is satisfying_Sh_1 )
assume  L is trivial ; ::_thesis: L is satisfying_Sh_1
then  for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | x)) = y by STRUCT_0:def_10;
hence  L is satisfying_Sh_1 by Def1; ::_thesis: verum
end;
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 )
proof
take  TrivShefferOrthoLattStr ; ::_thesis: ( TrivShefferOrthoLattStr is satisfying_Sh_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 )
thus  ( TrivShefferOrthoLattStr is satisfying_Sh_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 ) ; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: 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)
let x, y, z, u be Element of L; ::_thesis: ((x | (y | z)) | (x | (x | (y | z)))) | ((z | ((x | z) | z)) | (u | (x | (y | z)))) = z | ((x | z) | z)
set Y = z | ((x | z) | z);
set X = x | (y | z);
 ((x | (y | z)) | (((z | ((x | z) | z)) | (x | (y | z))) | (x | (y | z)))) | ((z | ((x | z) | z)) | (u | (x | (y | z)))) = z | ((x | z) | z) by Def1;
hence  ((x | (y | z)) | (x | (x | (y | z)))) | ((z | ((x | z) | z)) | (u | (x | (y | z)))) = z | ((x | z) | z) by Def1; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds ((x | y) | (((y | ((z | y) | y)) | (x | y)) | (x | y))) | z = y | ((z | y) | y)
let x, y, z be Element of L; ::_thesis: ((x | y) | (((y | ((z | y) | y)) | (x | y)) | (x | y))) | z = y | ((z | y) | y)
set X = x | y;
set Y = y | ((z | y) | y);
 ((x | y) | (((y | ((z | y) | y)) | (x | y)) | (x | y))) | ((y | ((z | y) | y)) | (z | (x | y))) = y | ((z | y) | y) by Def1;
hence  ((x | y) | (((y | ((z | y) | y)) | (x | y)) | (x | y))) | z = y | ((z | y) | y) by Def1; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | ((x | z) | z))) = y
let x, y, z be Element of L; ::_thesis: (x | ((y | x) | x)) | (y | (z | ((x | z) | z))) = y
set X = x | z;
set Y = z | ((x | z) | z);
 ((x | z) | (((z | ((x | z) | z)) | (x | z)) | (x | z))) | x = z | ((x | z) | z) by Th2;
hence  (x | ((y | x) | x)) | (y | (z | ((x | z) | z))) = y by Def1; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds x | ((x | ((x | x) | x)) | (y | (x | ((x | x) | x)))) = x | ((x | x) | x)
let x be Element of L; ::_thesis: for y being Element of L holds x | ((x | ((x | x) | x)) | (y | (x | ((x | x) | x)))) = x | ((x | x) | x)
 (x | ((x | x) | x)) | (x | (x | ((x | x) | x))) = x by Th3;
hence  for y being Element of L holds x | ((x | ((x | x) | x)) | (y | (x | ((x | x) | x)))) = x | ((x | x) | x) by Th1; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x being Element of L holds x | ((x | x) | x) = x | x
let x be Element of L; ::_thesis: x | ((x | x) | x) = x | x
 (x | ((x | x) | x)) | (x | (x | ((x | x) | x))) = x by Th3;
hence  x | ((x | x) | x) = x | x by Th4; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x being Element of L holds (x | ((x | x) | x)) | (x | x) = x
let x be Element of L; ::_thesis: (x | ((x | x) | x)) | (x | x) = x
 x | ((x | x) | x) = x | x by Th5;
hence  (x | ((x | x) | x)) | (x | x) = x by Def1; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds (x | x) | (x | (y | x)) = x
let x, y be Element of L; ::_thesis: (x | x) | (x | (y | x)) = x
 x | ((x | x) | x) = x | x by Th5;
hence  (x | x) | (x | (y | x)) = x by Def1; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds (x | (((y | y) | x) | x)) | y = y | y
let x, y be Element of L; ::_thesis: (x | (((y | y) | x) | x)) | y = y | y
set Y = y | y;
set X = x | y;
 (y | y) | (y | ((x | y) | y)) = y by Th7;
hence  (x | (((y | y) | x) | x)) | y = y | y by Th3; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: 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)
let x, y be Element of L; ::_thesis: ((x | y) | (((x | y) | (x | y)) | (x | y))) | ((x | y) | (x | y)) = y | ((((x | y) | (x | y)) | y) | y)
 (y | ((((x | y) | (x | y)) | y) | y)) | (x | y) = (x | y) | (x | y) by Th8;
hence  ((x | y) | (((x | y) | (x | y)) | (x | y))) | ((x | y) | (x | y)) = y | ((((x | y) | (x | y)) | y) | y) by Th2; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds x | ((((y | x) | (y | x)) | x) | x) = y | x
let x, y be Element of L; ::_thesis: x | ((((y | x) | (y | x)) | x) | x) = y | x
 ((y | x) | (((y | x) | (y | x)) | (y | x))) | ((y | x) | (y | x)) = y | x by Th6;
hence  x | ((((y | x) | (y | x)) | x) | x) = y | x by Th9; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds (x | x) | (y | x) = x
let x, y be Element of L; ::_thesis: (x | x) | (y | x) = x
set Y = y | x;
 x | ((((y | x) | (y | x)) | x) | x) = y | x by Th10;
hence  (x | x) | (y | x) = x by Th7; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds x | (y | (x | x)) = x | x
let x, y be Element of L; ::_thesis: x | (y | (x | x)) = x | x
set Y = x | x;
 (x | x) | (x | x) = x by Th11;
hence  x | (y | (x | x)) = x | x by Th11; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds ((x | y) | (x | y)) | y = x | y
let x, y be Element of L; ::_thesis: ((x | y) | (x | y)) | y = x | y
 (y | y) | (x | y) = y by Th11;
hence  ((x | y) | (x | y)) | y = x | y by Th11; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds x | ((y | x) | x) = y | x
let x, y be Element of L; ::_thesis: x | ((y | x) | x) = y | x
 ((y | x) | (y | x)) | x = y | x by Th13;
hence  x | ((y | x) | x) = y | x by Th10; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | y) | (x | (z | y)) = x
let x, y, z be Element of L; ::_thesis: (x | y) | (x | (z | y)) = x
 y | ((x | y) | y) = x | y by Th14;
hence  (x | y) | (x | (z | y)) = x by Def1; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | z)) | (x | z) = x
let x, y, z be Element of L; ::_thesis: (x | (y | z)) | (x | z) = x
 (z | z) | (y | z) = z by Th11;
hence  (x | (y | z)) | (x | z) = x by Th15; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | ((x | y) | (z | y)) = x | y
let x, y, z be Element of L; ::_thesis: x | ((x | y) | (z | y)) = x | y
 (x | y) | (x | (z | y)) = x by Th15;
hence  x | ((x | y) | (z | y)) = x | y by Th16; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds ((x | (y | z)) | z) | x = x | (y | z)
let x, y, z be Element of L; ::_thesis: ((x | (y | z)) | z) | x = x | (y | z)
set X = y | z;
 (x | (y | z)) | (x | z) = x by Th16;
hence  ((x | (y | z)) | z) | x = x | (y | z) by Th15; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds x | ((y | x) | x) = x | y
let x, y be Element of L; ::_thesis: x | ((y | x) | x) = x | y
 (x | ((y | x) | x)) | (y | ((y | x) | x)) = y by Def1;
hence  x | ((y | x) | x) = x | y by Th17; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds x | y = y | x
let x, y be Element of L; ::_thesis: x | y = y | x
 x | ((y | x) | x) = y | x by Th14;
hence  x | y = y | x by Th19; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds (x | y) | (x | x) = x
let x, y be Element of L; ::_thesis: (x | y) | (x | x) = x
set X = x | y;
 x | ((y | x) | x) = x | y by Th19;
hence  (x | y) | (x | x) = x by Th16; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | y) | (y | (z | x)) = y
let x, y, z be Element of L; ::_thesis: (x | y) | (y | (z | x)) = y
set Y = x | ((y | x) | x);
 x | ((y | x) | x) = x | y by Th19;
hence  (x | y) | (y | (z | x)) = y by Def1; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | z)) | (z | x) = x
let x, y, z be Element of L; ::_thesis: (x | (y | z)) | (z | x) = x
 z | x = x | z by Th20;
hence  (x | (y | z)) | (z | x) = x by Th16; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | y) | (y | (x | z)) = y
let x, y, z be Element of L; ::_thesis: (x | y) | (y | (x | z)) = y
 z | x = x | z by Th20;
hence  (x | y) | (y | (x | z)) = y by Th22; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | z)) | (y | x) = x
let x, y, z be Element of L; ::_thesis: (x | (y | z)) | (y | x) = x
 z | y = y | z by Th20;
hence  (x | (y | z)) | (y | x) = x by Th23; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds ((x | y) | (x | z)) | z = x | z
let x, y, z be Element of L; ::_thesis: ((x | y) | (x | z)) | z = x | z
 (x | z) | (z | (x | y)) = z by Th24;
hence  ((x | y) | (x | z)) | z = x | z by Th22; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | (y | (x | (y | z))) = x | (y | z)
let x, y, z be Element of L; ::_thesis: x | (y | (x | (y | z))) = x | (y | z)
set Y = y | x;
 (x | (y | z)) | (y | x) = x by Th25;
hence  x | (y | (x | (y | z))) = x | (y | z) by Th25; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (x | z)
let x, y, z be Element of L; ::_thesis: (x | (y | (x | z))) | y = y | (x | z)
set Y = y | (x | z);
 (y | (x | z)) | (x | y) = y by Th25;
hence  (x | (y | (x | z))) | y = y | (x | z) by Th24; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z, u being Element of L holds (x | (y | z)) | (x | (u | (y | x))) = (x | (y | z)) | (y | x)
let x, y, z, u be Element of L; ::_thesis: (x | (y | z)) | (x | (u | (y | x))) = (x | (y | z)) | (y | x)
set X = x | (y | z);
set Y = y | x;
 (x | (y | z)) | (y | x) = x by Th25;
hence  (x | (y | z)) | (x | (u | (y | x))) = (x | (y | z)) | (y | x) by Th17; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (z | x)
let x, y, z be Element of L; ::_thesis: (x | (y | (x | z))) | y = y | (z | x)
 z | x = x | z by Th20;
hence  (x | (y | (x | z))) | y = y | (z | x) by Th28; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z, u being Element of L holds (x | (y | z)) | (x | (u | (y | x))) = x
let x, y, z be Element of L; ::_thesis: for u being Element of L holds (x | (y | z)) | (x | (u | (y | x))) = x
 (x | (y | z)) | (y | x) = x by Th25;
hence  for u being Element of L holds (x | (y | z)) | (x | (u | (y | x))) = x by Th29; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds x | (y | (x | y)) = x | x
let x, y be Element of L; ::_thesis: x | (y | (x | y)) = x | x
 (x | y) | (x | ((x | y) | y)) = x by Th15;
hence  x | (y | (x | y)) = x | x by Th30; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | (y | z) = x | (z | y)
let x, y, z be Element of L; ::_thesis: x | (y | z) = x | (z | y)
 (z | (x | (z | y))) | x = x | (z | y) by Th28;
hence  x | (y | z) = x | (z | y) by Th30; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | (y | (x | (z | (y | x)))) = x | x
let x, y, z be Element of L; ::_thesis: x | (y | (x | (z | (y | x)))) = x | x
 (x | (y | (x | (z | (y | x))))) | (x | (z | (y | x))) = x by Th31;
hence  x | (y | (x | (z | (y | x)))) = x | x by Th18; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | z)) | ((y | x) | x) = (x | (y | z)) | (x | (y | z))
let x, y, z be Element of L; ::_thesis: (x | (y | z)) | ((y | x) | x) = (x | (y | z)) | (x | (y | z))
set X = x | (y | z);
 (x | (y | z)) | (y | x) = x by Th25;
hence  (x | (y | z)) | ((y | x) | x) = (x | (y | z)) | (x | (y | z)) by Th32; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds (x | (y | x)) | y = y | y
let x, y be Element of L; ::_thesis: (x | (y | x)) | y = y | y
set X = x;
set Y = y;
 y | (x | (y | x)) = (x | (y | x)) | y by Th20;
hence  (x | (y | x)) | y = y | y by Th32; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | y) | z = z | (y | x)
let x, y, z be Element of L; ::_thesis: (x | y) | z = z | (y | x)
set X = x | y;
 (x | y) | z = z | (x | y) by Th20;
hence  (x | y) | z = z | (y | x) by Th33; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | (y | (z | (x | y))) = x | (y | y)
let x, y, z be Element of L; ::_thesis: x | (y | (z | (x | y))) = x | (y | y)
set Y = z;
 y | (x | (y | (z | (x | y)))) = y | y by Th34;
hence  x | (y | (z | (x | y))) = x | (y | y) by Th27; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds ((x | y) | y) | (y | (z | x)) = (y | (z | x)) | (y | (z | x))
let x, y, z be Element of L; ::_thesis: ((x | y) | y) | (y | (z | x)) = (y | (z | x)) | (y | (z | x))
set X = y | (z | x);
 (y | (z | x)) | (x | y) = y by Th23;
hence  ((x | y) | y) | (y | (z | x)) = (y | (z | x)) | (y | (z | x)) by Th36; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z, u being Element of L holds (x | y) | (z | u) = (u | z) | (y | x)
let x, y, z, u be Element of L; ::_thesis: (x | y) | (z | u) = (u | z) | (y | x)
 (x | y) | (z | u) = (x | y) | (u | z) by Th33;
hence  (x | y) | (z | u) = (u | z) | (y | x) by Th37; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | (y | ((y | x) | z)) = x | (y | y)
let x, y, z be Element of L; ::_thesis: x | (y | ((y | x) | z)) = x | (y | y)
 x | (y | (z | (x | y))) = x | (y | ((y | x) | z)) by Th37;
hence  x | (y | ((y | x) | z)) = x | (y | y) by Th38; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds x | (y | x) = x | (y | y)
let x, y be Element of L; ::_thesis: x | (y | x) = x | (y | y)
set Y = x | (y | y);
 (x | (y | y)) | (x | y) = x by Th16;
hence  x | (y | x) = x | (y | y) by Th38; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds (x | y) | y = y | (x | x)
let x, y be Element of L; ::_thesis: (x | y) | y = y | (x | x)
set X = x;
set Y = y;
 y | (x | y) = (x | y) | y by Th20;
hence  (x | y) | y = y | (x | x) by Th42; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds x | (y | y) = x | (x | y)
let x, y be Element of L; ::_thesis: x | (y | y) = x | (x | y)
 x | (y | x) = x | (y | y) by Th42;
hence  x | (y | y) = x | (x | y) by Th33; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | y)) | (x | (z | y)) = (x | (z | y)) | (x | (z | y))
let x, y, z be Element of L; ::_thesis: (x | (y | y)) | (x | (z | y)) = (x | (z | y)) | (x | (z | y))
set Y = y;
set X = x;
 (y | x) | x = x | (y | y) by Th43;
hence  (x | (y | y)) | (x | (z | y)) = (x | (z | y)) | (x | (z | y)) by Th39; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | z)) | (x | (y | y)) = (x | (y | z)) | (x | (y | z))
let x, y, z be Element of L; ::_thesis: (x | (y | z)) | (x | (y | y)) = (x | (y | z)) | (x | (y | z))
 (x | (y | z)) | ((y | x) | x) = (x | (y | z)) | (x | (y | y)) by Th43;
hence  (x | (y | z)) | (x | (y | y)) = (x | (y | z)) | (x | (y | z)) by Th35; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x | y)))) = x | ((y | y) | (y | y))
let x, y, z be Element of L; ::_thesis: x | ((y | y) | (z | (x | (x | y)))) = x | ((y | y) | (y | y))
 x | (y | y) = x | (x | y) by Th44;
hence  x | ((y | y) | (z | (x | (x | y)))) = x | ((y | y) | (y | y)) by Th38; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds ((x | (y | z)) | (x | (y | z))) | (y | y) = x | (y | y)
let x, y, z be Element of L; ::_thesis: ((x | (y | z)) | (x | (y | z))) | (y | y) = x | (y | y)
set Z = y | y;
set Y = y | z;
 (x | (y | z)) | (x | (y | z)) = (x | (y | z)) | (x | (y | y)) by Th46;
hence  ((x | (y | z)) | (x | (y | z))) | (y | y) = x | (y | y) by Th26; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x | y)))) = x | y
let x, y, z be Element of L; ::_thesis: x | ((y | y) | (z | (x | (x | y)))) = x | y
 (y | y) | (y | y) = y by Th21;
hence  x | ((y | y) | (z | (x | (x | y)))) = x | y by Th47; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: 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)
let x, y, z be Element of L; ::_thesis: (((x | y) | (x | y)) | ((z | ((x | y) | z)) | (x | y))) | (x | x) = (z | ((x | y) | z)) | (x | x)
set Y = z;
set X = x | y;
 (z | ((x | y) | z)) | (x | y) = (x | y) | (x | y) by Th36;
hence  (((x | y) | (x | y)) | ((z | ((x | y) | z)) | (x | y))) | (x | x) = (z | ((x | y) | z)) | (x | x) by Th48; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = (y | z) | (y | y)
let x, y, z be Element of L; ::_thesis: (x | ((y | z) | x)) | (y | y) = (y | z) | (y | y)
set Y = y | z;
set X = x | ((y | z) | x);
 ((y | z) | (y | z)) | ((x | ((y | z) | x)) | (y | z)) = y | z by Th11;
hence  (x | ((y | z) | x)) | (y | y) = (y | z) | (y | y) by Th50; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = y
let x, y, z be Element of L; ::_thesis: (x | ((y | z) | x)) | (y | y) = y
 (y | z) | (y | y) = y by Th21;
hence  (x | ((y | z) | x)) | (y | y) = y by Th51; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | ((y | ((x | z) | y)) | x) = y | ((x | z) | y)
let x, y, z be Element of L; ::_thesis: x | ((y | ((x | z) | y)) | x) = y | ((x | z) | y)
 (y | ((x | z) | y)) | (x | x) = x by Th52;
hence  x | ((y | ((x | z) | y)) | x) = y | ((x | z) | y) by Th16; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | ((y | (y | (z | x))) | x) = y | ((x | (y | (x | z))) | y)
let x, y, z be Element of L; ::_thesis: x | ((y | (y | (z | x))) | x) = y | ((x | (y | (x | z))) | y)
set Z = y | (x | z);
 (x | (y | (x | z))) | y = y | (z | x) by Th30;
hence  x | ((y | (y | (z | x))) | x) = y | ((x | (y | (x | z))) | y) by Th53; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | ((y | (y | (z | x))) | x) = y | (y | (z | x))
let x, y, z be Element of L; ::_thesis: x | ((y | (y | (z | x))) | x) = y | (y | (z | x))
 y | (z | x) = (x | (y | (x | z))) | y by Th30;
hence  x | ((y | (y | (z | x))) | x) = y | (y | (z | x)) by Th54; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z, u being Element of L holds x | (y | (z | (z | (u | (y | x))))) = x | (y | y)
let x, y, z, u be Element of L; ::_thesis: x | (y | (z | (z | (u | (y | x))))) = x | (y | y)
 (y | x) | ((z | (z | (u | (y | x)))) | (y | x)) = z | (z | (u | (y | x))) by Th55;
hence  x | (y | (z | (z | (u | (y | x))))) = x | (y | y) by Th41; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | (y | (y | (z | (x | y)))) = x | (y | (x | x))
let x, y, z be Element of L; ::_thesis: x | (y | (y | (z | (x | y)))) = x | (y | (x | x))
 y | (x | (y | (y | (z | (x | y))))) = y | (x | x) by Th56;
hence  x | (y | (y | (z | (x | y)))) = x | (y | (x | x)) by Th27; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | (y | (y | (z | (x | y)))) = x | x
let x, y, z be Element of L; ::_thesis: x | (y | (y | (z | (x | y)))) = x | x
 x | (y | (x | x)) = x | x by Th12;
hence  x | (y | (y | (z | (x | y)))) = x | x by Th57; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y being Element of L holds x | (y | (y | y)) = x | x
let x, y be Element of L; ::_thesis: x | (y | (y | y)) = x | x
set Y = y | (x | y);
 (y | (x | y)) | (x | y) = y by Th25;
hence  x | (y | (y | y)) = x | x by Th58; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | (((y | (z | x)) | (y | (z | x))) | (z | z)) = x | (y | (z | x))
let x, y, z be Element of L; ::_thesis: x | (((y | (z | x)) | (y | (z | x))) | (z | z)) = x | (y | (z | x))
set Y = y | (z | x);
 z | (x | (x | (y | (z | x)))) = z | z by Th58;
hence  x | (((y | (z | x)) | (y | (z | x))) | (z | z)) = x | (y | (z | x)) by Th49; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | (y | (z | z)) = x | (y | (z | x))
let x, y, z be Element of L; ::_thesis: x | (y | (z | z)) = x | (y | (z | x))
 ((y | (z | x)) | (y | (z | x))) | (z | z) = y | (z | z) by Th48;
hence  x | (y | (z | z)) = x | (y | (z | x)) by Th60; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds x | (y | ((z | z) | x)) = x | (y | z)
let x, y, z be Element of L; ::_thesis: x | (y | ((z | z) | x)) = x | (y | z)
set X = z | z;
 (z | z) | (z | z) = z by Th21;
hence  x | (y | ((z | z) | x)) = x | (y | z) by Th61; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | y)) | (x | (z | ((y | y) | x))) = (x | (z | y)) | (x | (z | y))
let x, y, z be Element of L; ::_thesis: (x | (y | y)) | (x | (z | ((y | y) | x))) = (x | (z | y)) | (x | (z | y))
 x | (z | ((y | y) | x)) = x | (z | y) by Th62;
hence  (x | (y | y)) | (x | (z | ((y | y) | x))) = (x | (z | y)) | (x | (z | y)) by Th45; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | y)) | (x | (z | (x | (y | y)))) = (x | (z | y)) | (x | (z | y))
let x, y, z be Element of L; ::_thesis: (x | (y | y)) | (x | (z | (x | (y | y)))) = (x | (z | y)) | (x | (z | y))
 x | (y | y) = (y | y) | x by Th37;
hence  (x | (y | y)) | (x | (z | (x | (y | y)))) = (x | (z | y)) | (x | (z | y)) by Th63; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds (x | (y | y)) | (x | (z | z)) = (x | (z | y)) | (x | (z | y))
let x, y, z be Element of L; ::_thesis: (x | (y | y)) | (x | (z | z)) = (x | (z | y)) | (x | (z | y))
set X = x | (y | y);
 (x | (y | y)) | (x | (z | z)) = (x | (y | y)) | (x | (z | (x | (y | y)))) by Th61;
hence  (x | (y | y)) | (x | (z | z)) = (x | (z | y)) | (x | (z | y)) by Th64; ::_thesis: verum
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
let L be non empty satisfying_Sh_1 ShefferStr ; ::_thesis: for x, y, z being Element of L holds ((x | x) | y) | ((z | z) | y) = (y | (x | z)) | (y | (x | z))
let x, y, z be Element of L; ::_thesis: ((x | x) | y) | ((z | z) | y) = (y | (x | z)) | (y | (x | z))
 (y | (z | z)) | (y | (x | x)) = ((x | x) | y) | ((z | z) | y) by Th40;
hence  ((x | x) | y) | ((z | z) | y) = (y | (x | z)) | (y | (x | z)) by Th65; ::_thesis: verum
end;

theorem Th67: :: SHEFFER2:67
for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_1
proof
let L be non empty ShefferStr ; ::_thesis: ( L is satisfying_Sh_1 implies L is satisfying_Sheffer_1 )
assume  L is satisfying_Sh_1 ; ::_thesis: L is satisfying_Sheffer_1
then  for x being Element of L holds (x | x) | (x | x) = x by Th21;
hence  L is satisfying_Sheffer_1 by SHEFFER1:def_13; ::_thesis: verum
end;

theorem Th68: :: SHEFFER2:68
for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_2
proof
let L be non empty ShefferStr ; ::_thesis: ( L is satisfying_Sh_1 implies L is satisfying_Sheffer_2 )
assume  L is satisfying_Sh_1 ; ::_thesis: L is satisfying_Sheffer_2
then  for x, y being Element of L holds x | (y | (y | y)) = x | x by Th59;
hence  L is satisfying_Sheffer_2 by SHEFFER1:def_14; ::_thesis: verum
end;

theorem Th69: :: SHEFFER2:69
for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_3
proof
let L be non empty ShefferStr ; ::_thesis: ( L is satisfying_Sh_1 implies L is satisfying_Sheffer_3 )
assume  L is satisfying_Sh_1 ; ::_thesis: L is satisfying_Sheffer_3
then  for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) by Th66;
hence  L is satisfying_Sheffer_3 by SHEFFER1:def_15; ::_thesis: verum
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 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 )
proof
take  TrivShefferOrthoLattStr ; ::_thesis: ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is Boolean & TrivShefferOrthoLattStr is well-complemented & TrivShefferOrthoLattStr is Lattice-like & TrivShefferOrthoLattStr is de_Morgan & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 & TrivShefferOrthoLattStr is satisfying_Sh_1 )
 for x, y being Element of TrivShefferOrthoLattStr holds x "/\" y = ((x `) "\/" (y `)) ` by STRUCT_0:def_10;
hence  ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is Boolean & TrivShefferOrthoLattStr is well-complemented & TrivShefferOrthoLattStr is Lattice-like & TrivShefferOrthoLattStr is de_Morgan & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 & TrivShefferOrthoLattStr is satisfying_Sh_1 ) by ROBBINS1:def_23; ::_thesis: verum
end;
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
proof
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, w being Element of L holds w | ((x | x) | x) = w | w
let x, w be Element of L; ::_thesis: w | ((x | x) | x) = w | w
 (x | x) | (x | x) = x by SHEFFER1:def_13;
hence  w | ((x | x) | x) = w | w by SHEFFER1:def_14; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, x being Element of L holds x = (x | x) | (p | (p | p))
let p, x be Element of L; ::_thesis: x = (x | x) | (p | (p | p))
 (x | x) | (x | x) = x by SHEFFER1:def_13;
hence  x = (x | x) | (p | (p | p)) by SHEFFER1:def_14; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for y, w being Element of L holds (w | w) | (w | (y | (y | y))) = w
let y, w be Element of L; ::_thesis: (w | w) | (w | (y | (y | y))) = w
 w | w = w | (y | (y | y)) by SHEFFER1:def_14;
hence  (w | w) | (w | (y | (y | y))) = w by SHEFFER1:def_13; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for q, p, y, w being Element of L holds ((w | (y | (y | y))) | p) | ((q | q) | p) = (p | (w | q)) | (p | (w | q))
let q, p, y, w be Element of L; ::_thesis: ((w | (y | (y | y))) | p) | ((q | q) | p) = (p | (w | q)) | (p | (w | q))
 w | w = w | (y | (y | y)) by SHEFFER1:def_14;
hence  ((w | (y | (y | y))) | p) | ((q | q) | p) = (p | (w | q)) | (p | (w | q)) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for q, p, x being Element of L holds (x | p) | ((q | q) | p) = (p | ((x | x) | q)) | (p | ((x | x) | q))
let q, p, x be Element of L; ::_thesis: (x | p) | ((q | q) | p) = (p | ((x | x) | q)) | (p | ((x | x) | q))
 (x | x) | (x | x) = x by SHEFFER1:def_13;
hence  (x | p) | ((q | q) | p) = (p | ((x | x) | q)) | (p | ((x | x) | q)) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, p, y, q being Element of L holds ((w | w) | p) | ((q | (y | (y | y))) | p) = (p | (w | q)) | (p | (w | q))
let w, p, y, q be Element of L; ::_thesis: ((w | w) | p) | ((q | (y | (y | y))) | p) = (p | (w | q)) | (p | (w | q))
 q | q = q | (y | (y | y)) by SHEFFER1:def_14;
hence  ((w | w) | p) | ((q | (y | (y | y))) | p) = (p | (w | q)) | (p | (w | q)) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, x being Element of L holds x = (x | x) | ((p | p) | p)
let p, x be Element of L; ::_thesis: x = (x | x) | ((p | p) | p)
 (x | x) | (x | x) = x by SHEFFER1:def_13;
hence  x = (x | x) | ((p | p) | p) by Th70; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for y, w being Element of L holds (w | w) | (w | ((y | y) | y)) = w
let y, w be Element of L; ::_thesis: (w | w) | (w | ((y | y) | y)) = w
 w | w = w | ((y | y) | y) by Th70;
hence  (w | w) | (w | ((y | y) | y)) = w by SHEFFER1:def_13; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for y, w being Element of L holds (w | ((y | y) | y)) | (w | w) = w
let y, w be Element of L; ::_thesis: (w | ((y | y) | y)) | (w | w) = w
 w | w = w | ((y | y) | y) by Th70;
hence  (w | ((y | y) | y)) | (w | w) = w by SHEFFER1:def_13; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, y, w being Element of L holds (w | ((y | y) | y)) | (p | (p | p)) = w
let p, y, w be Element of L; ::_thesis: (w | ((y | y) | y)) | (p | (p | p)) = w
 w | w = w | ((y | y) | y) by Th70;
hence  (w | ((y | y) | y)) | (p | (p | p)) = w by Th71; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, x, y being Element of L holds ((y | (x | x)) | (y | (x | x))) | (p | (p | p)) = (x | x) | y
let p, x, y be Element of L; ::_thesis: ((y | (x | x)) | (y | (x | x))) | (p | (p | p)) = (x | x) | y
 ((x | x) | y) | ((x | x) | y) = (y | (x | x)) | (y | (x | x)) by SHEFFER1:def_15;
hence  ((y | (x | x)) | (y | (x | x))) | (p | (p | p)) = (x | x) | y by Th71; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, y being Element of L holds y | (x | x) = (x | x) | y
now__::_thesis:_for_p,_x,_y_being_Element_of_L_holds_y_|_(x_|_x)_=_(x_|_x)_|_y
let p, x, y be Element of L; ::_thesis: y | (x | x) = (x | x) | y
 ((y | (x | x)) | (y | (x | x))) | (p | (p | p)) = y | (x | x) by Th71;
hence  y | (x | x) = (x | x) | y by Th80; ::_thesis: verum
end;
hence  for x, y being Element of L holds y | (x | x) = (x | x) | y ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for y, w being Element of L holds w | y = ((y | y) | (y | y)) | w
let y, w be Element of L; ::_thesis: w | y = ((y | y) | (y | y)) | w
 (y | y) | (y | y) = y by SHEFFER1:def_13;
hence  w | y = ((y | y) | (y | y)) | w by Th81; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for y, w being Element of L holds w | y = y | w
let y, w be Element of L; ::_thesis: w | y = y | w
 (y | y) | (y | y) = y by SHEFFER1:def_13;
hence  w | y = y | w by Th82; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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)
let x, p be Element of L; ::_thesis: (p | x) | (p | ((x | x) | (x | x))) = (((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p)
 (x | x) | (x | x) = x by SHEFFER1:def_13;
hence  (p | x) | (p | ((x | x) | (x | x))) = (((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, p being Element of L holds (p | x) | (p | x) = (((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p)
let x, p be Element of L; ::_thesis: (p | x) | (p | x) = (((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p)
 (x | x) | (x | x) = x by SHEFFER1:def_13;
hence  (p | x) | (p | x) = (((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p) by Th84; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, p being Element of L holds (p | x) | (p | x) = (x | p) | (((x | x) | (x | x)) | p)
let x, p be Element of L; ::_thesis: (p | x) | (p | x) = (x | p) | (((x | x) | (x | x)) | p)
 (x | x) | (x | x) = x by SHEFFER1:def_13;
hence  (p | x) | (p | x) = (x | p) | (((x | x) | (x | x)) | p) by Th85; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, p being Element of L holds (p | x) | (p | x) = (x | p) | (x | p)
let x, p be Element of L; ::_thesis: (p | x) | (p | x) = (x | p) | (x | p)
 (x | x) | (x | x) = x by SHEFFER1:def_13;
hence  (p | x) | (p | x) = (x | p) | (x | p) by Th86; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let y, q, w be Element of L; ::_thesis: ((w | q) | ((y | y) | y)) | ((w | q) | (w | q)) = ((w | w) | (w | q)) | ((q | q) | (w | q))
 (w | q) | (w | q) = (w | q) | ((y | y) | y) by Th70;
hence  ((w | q) | ((y | y) | y)) | ((w | q) | (w | q)) = ((w | w) | (w | q)) | ((q | q) | (w | q)) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for q, w being Element of L holds w | q = ((w | w) | (w | q)) | ((q | q) | (w | q))
now__::_thesis:_for_y,_q,_w_being_Element_of_L_holds_w_|_q_=_((w_|_w)_|_(w_|_q))_|_((q_|_q)_|_(w_|_q))
let y, q, w be Element of L; ::_thesis: w | q = ((w | w) | (w | q)) | ((q | q) | (w | q))
 ((w | q) | ((y | y) | y)) | ((w | q) | (w | q)) = w | q by Th78;
hence  w | q = ((w | w) | (w | q)) | ((q | q) | (w | q)) by Th88; ::_thesis: verum
end;
hence  for q, w being Element of L holds w | q = ((w | w) | (w | q)) | ((q | q) | (w | q)) ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for q, p being Element of L holds (p | p) | (p | ((q | q) | q)) = (((q | q) | (q | q)) | p) | ((q | q) | p)
let q, p be Element of L; ::_thesis: (p | p) | (p | ((q | q) | q)) = (((q | q) | (q | q)) | p) | ((q | q) | p)
 p | ((q | q) | q) = p | p by Th70;
hence  (p | p) | (p | ((q | q) | q)) = (((q | q) | (q | q)) | p) | ((q | q) | p) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, q being Element of L holds p = (((q | q) | (q | q)) | p) | ((q | q) | p)
let p, q be Element of L; ::_thesis: p = (((q | q) | (q | q)) | p) | ((q | q) | p)
 (p | p) | (p | ((q | q) | q)) = p by Th77;
hence  p = (((q | q) | (q | q)) | p) | ((q | q) | p) by Th90; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, q being Element of L holds p = (q | p) | ((q | q) | p)
let p, q be Element of L; ::_thesis: p = (q | p) | ((q | q) | p)
 (q | q) | (q | q) = q by SHEFFER1:def_13;
hence  p = (q | p) | ((q | q) | p) by Th91; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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)))
let z, w, x be Element of L; ::_thesis: (((x | x) | w) | ((z | z) | w)) | ((w | (x | z)) | (w | (x | z))) = ((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w | (x | z)))
 (w | (x | z)) | (w | (x | z)) = ((x | x) | w) | ((z | z) | w) by SHEFFER1:def_15;
hence  (((x | x) | w) | ((z | z) | w)) | ((w | (x | z)) | (w | (x | z))) = ((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w | (x | z))) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for z, w, x being Element of L holds (((x | x) | w) | ((z | z) | w)) | ((w | (x | z)) | (w | (x | z))) = w | (x | z)
let z, w, x be Element of L; ::_thesis: (((x | x) | w) | ((z | z) | w)) | ((w | (x | z)) | (w | (x | z))) = w | (x | z)
 ((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w | (x | z))) = w | (x | z) by Th89;
hence  (((x | x) | w) | ((z | z) | w)) | ((w | (x | z)) | (w | (x | z))) = w | (x | z) by Th93; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, p being Element of L holds (p | p) | (p | (w | (w | w))) = ((w | w) | p) | (((w | w) | (w | w)) | p)
let w, p be Element of L; ::_thesis: (p | p) | (p | (w | (w | w))) = ((w | w) | p) | (((w | w) | (w | w)) | p)
 p | (w | (w | w)) = p | p by SHEFFER1:def_14;
hence  (p | p) | (p | (w | (w | w))) = ((w | w) | p) | (((w | w) | (w | w)) | p) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, w being Element of L holds p = ((w | w) | p) | (((w | w) | (w | w)) | p)
let p, w be Element of L; ::_thesis: p = ((w | w) | p) | (((w | w) | (w | w)) | p)
 (p | p) | (p | (w | (w | w))) = p by Th72;
hence  p = ((w | w) | p) | (((w | w) | (w | w)) | p) by Th95; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, w being Element of L holds p = ((w | w) | p) | (w | p)
let p, w be Element of L; ::_thesis: p = ((w | w) | p) | (w | p)
 (w | w) | (w | w) = w by SHEFFER1:def_13;
hence  p = ((w | w) | p) | (w | p) by Th96; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let z, q, x be Element of L; ::_thesis: (((x | x) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z))) = (((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q))
 ((x | x) | q) | ((z | z) | q) = (q | (x | z)) | (q | (x | z)) by SHEFFER1:def_15;
hence  (((x | x) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z))) = (((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q)) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for q, z, x being Element of L holds q | (x | z) = (((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q))
let q, z, x be Element of L; ::_thesis: q | (x | z) = (((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q))
 (((x | x) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z))) = q | (x | z) by Th94;
hence  q | (x | z) = (((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q)) by Th98; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for q, z, x being Element of L holds q | (x | z) = (z | ((x | x) | q)) | ((q | q) | ((x | x) | q))
let q, z, x be Element of L; ::_thesis: q | (x | z) = (z | ((x | x) | q)) | ((q | q) | ((x | x) | q))
 (z | z) | (z | z) = z by SHEFFER1:def_13;
hence  q | (x | z) = (z | ((x | x) | q)) | ((q | q) | ((x | x) | q)) by Th99; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, y being Element of L holds w | w = ((y | y) | y) | w
let w, y be Element of L; ::_thesis: w | w = ((y | y) | y) | w
 w | ((y | y) | y) = w | w by Th70;
hence  w | w = ((y | y) | y) | w by Th83; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, p being Element of L holds (p | w) | ((w | w) | p) = p
let w, p be Element of L; ::_thesis: (p | w) | ((w | w) | p) = p
 w | p = p | w by Th83;
hence  (p | w) | ((w | w) | p) = p by Th92; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for y, w being Element of L holds (w | w) | ((w | w) | ((y | y) | y)) = (y | y) | y
let y, w be Element of L; ::_thesis: (w | w) | ((w | w) | ((y | y) | y)) = (y | y) | y
 w | ((y | y) | y) = w | w by Th70;
hence  (w | w) | ((w | w) | ((y | y) | y)) = (y | y) | y by Th92; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for y, w being Element of L holds (w | w) | w = (y | y) | y
let y, w be Element of L; ::_thesis: (w | w) | w = (y | y) | y
 (w | w) | ((y | y) | y) = w by Th76;
hence  (w | w) | w = (y | y) | y by Th103; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, w being Element of L holds (w | p) | (p | (w | w)) = p
let p, w be Element of L; ::_thesis: (w | p) | (p | (w | w)) = p
 (w | w) | p = p | (w | w) by Th83;
hence  (w | p) | (p | (w | w)) = p by Th92; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, p being Element of L holds (p | (w | w)) | (w | p) = p
let w, p be Element of L; ::_thesis: (p | (w | w)) | (w | p) = p
 (w | w) | p = p | (w | w) by Th83;
hence  (p | (w | w)) | (w | p) = p by Th97; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, w being Element of L holds (w | p) | (w | (p | p)) = w
let p, w be Element of L; ::_thesis: (w | p) | (w | (p | p)) = w
 (p | p) | w = w | (p | p) by Th83;
hence  (w | p) | (w | (p | p)) = w by Th102; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, y being Element of L holds y | (((y | (x | x)) | (y | (x | x))) | (x | y)) = x | y
let x, y be Element of L; ::_thesis: y | (((y | (x | x)) | (y | (x | x))) | (x | y)) = x | y
 (x | y) | (y | (x | x)) = y by Th105;
hence  y | (((y | (x | x)) | (y | (x | x))) | (x | y)) = x | y by Th102; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, w being Element of L holds (w | (p | p)) | (w | p) = w
let p, w be Element of L; ::_thesis: (w | (p | p)) | (w | p) = w
 p | w = w | p by Th83;
hence  (w | (p | p)) | (w | p) = w by Th106; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let p, w, q, y be Element of L; ::_thesis: (((y | y) | y) | q) | ((w | w) | q) = (q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w))
 ((p | (p | p)) | (p | (p | p))) | (p | (p | p)) = (y | y) | y by Th104;
hence  (((y | y) | y) | q) | ((w | w) | q) = (q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w)) by Th73; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let q, w, p be Element of L; ::_thesis: (q | q) | ((w | w) | q) = (q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w))
 (((p | (p | p)) | (p | (p | p))) | (p | (p | p))) | q = q | q by Th101;
hence  (q | q) | ((w | w) | q) = (q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w)) by Th73; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, y, p being Element of L holds (w | p) | (w | (p | (y | (y | y)))) = w
let w, y, p be Element of L; ::_thesis: (w | p) | (w | (p | (y | (y | y)))) = w
 p | p = p | (y | (y | y)) by SHEFFER1:def_14;
hence  (w | p) | (w | (p | (y | (y | y)))) = w by Th107; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, y, p being Element of L holds (w | (p | (y | (y | y)))) | (w | p) = w
let w, y, p be Element of L; ::_thesis: (w | (p | (y | (y | y)))) | (w | p) = w
 p | p = p | (y | (y | y)) by SHEFFER1:def_14;
hence  (w | (p | (y | (y | y)))) | (w | p) = w by Th109; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for q, p, y being Element of L holds (((y | y) | y) | p) | ((q | q) | p) = (p | ((p | p) | q)) | (p | ((p | p) | q))
let q, p, y be Element of L; ::_thesis: (((y | y) | y) | p) | ((q | q) | p) = (p | ((p | p) | q)) | (p | ((p | p) | q))
 p | p = ((y | y) | y) | p by Th101;
hence  (((y | y) | y) | p) | ((q | q) | p) = (p | ((p | p) | q)) | (p | ((p | p) | q)) by Th74; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let q, z, x be Element of L; ::_thesis: ((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q)) = (((z | z) | (z | z)) | (x | q)) | ((q | q) | (x | q))
 (x | q) | ((z | z) | q) = (q | ((x | x) | z)) | (q | ((x | x) | z)) by Th74;
hence  ((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q)) = (((z | z) | (z | z)) | (x | q)) | ((q | q) | (x | q)) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let q, z, x be Element of L; ::_thesis: ((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q)) = (z | (x | q)) | ((q | q) | (x | q))
 (z | z) | (z | z) = z by SHEFFER1:def_13;
hence  ((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q)) = (z | (x | q)) | ((q | q) | (x | q)) by Th115; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let w, q, z be Element of L; ::_thesis: ((w | w) | ((z | z) | q)) | ((q | ((q | q) | z)) | (q | ((q | q) | z))) = (((z | z) | q) | (w | q)) | (((z | z) | q) | (w | q))
 (q | q) | ((z | z) | q) = (q | ((q | q) | z)) | (q | ((q | q) | z)) by Th74;
hence  ((w | w) | ((z | z) | q)) | ((q | ((q | q) | z)) | (q | ((q | q) | z))) = (((z | z) | q) | (w | q)) | (((z | z) | q) | (w | q)) by SHEFFER1:def_15; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for q, p, x being Element of L holds ((p | (x | p)) | (p | (x | p))) | (q | (q | q)) = (x | x) | p
let q, p, x be Element of L; ::_thesis: ((p | (x | p)) | (p | (x | p))) | (q | (q | q)) = (x | x) | p
 ((x | x) | p) | ((p | p) | p) = (p | (x | p)) | (p | (x | p)) by SHEFFER1:def_15;
hence  ((p | (x | p)) | (p | (x | p))) | (q | (q | q)) = (x | x) | p by Th79; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, x being Element of L holds p | (x | p) = (x | x) | p
now__::_thesis:_for_q,_p,_x_being_Element_of_L_holds_p_|_(x_|_p)_=_(x_|_x)_|_p
let q, p, x be Element of L; ::_thesis: p | (x | p) = (x | x) | p
 ((p | (x | p)) | (p | (x | p))) | (q | (q | q)) = p | (x | p) by Th71;
hence  p | (x | p) = (x | x) | p by Th118; ::_thesis: verum
end;
hence  for p, x being Element of L holds p | (x | p) = (x | x) | p ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, y being Element of L holds (y | p) | ((y | y) | p) = (p | p) | (y | p)
let p, y be Element of L; ::_thesis: (y | p) | ((y | y) | p) = (p | p) | (y | p)
 p | (y | p) = (y | y) | p by Th119;
hence  (y | p) | ((y | y) | p) = (p | p) | (y | p) by Th119; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, y being Element of L holds x = (x | x) | (y | x)
let x, y be Element of L; ::_thesis: x = (x | x) | (y | x)
 (y | x) | ((y | y) | x) = x by Th92;
hence  x = (x | x) | (y | x) by Th120; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, y being Element of L holds (y | x) | x = ((x | (y | y)) | (x | (y | y))) | (y | x)
let x, y be Element of L; ::_thesis: (y | x) | x = ((x | (y | y)) | (x | (y | y))) | (y | x)
 (x | (y | y)) | (y | x) = x by Th106;
hence  (y | x) | x = ((x | (y | y)) | (x | (y | y))) | (y | x) by Th119; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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
let x, z, y be Element of L; ::_thesis: ((x | ((y | y) | z)) | (x | ((y | y) | z))) | ((y | x) | ((z | z) | x)) = (z | (y | x)) | x
 (x | x) | (y | x) = x by Th121;
hence  ((x | ((y | y) | z)) | (x | ((y | y) | z))) | ((y | x) | ((z | z) | x)) = (z | (y | x)) | x by Th116; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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
let x, y, z be Element of L; ::_thesis: (x | (((z | (z | z)) | (z | (z | z))) | y)) | (x | (((z | (z | z)) | (z | (z | z))) | y)) = x
 (x | x) | ((y | y) | x) = x by Th121;
hence  (x | (((z | (z | z)) | (z | (z | z))) | y)) | (x | (((z | (z | z)) | (z | (z | z))) | y)) = x by Th111; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, z, y being Element of L holds (x | ((y | y) | z)) | z = z | (y | x)
let x, z, y be Element of L; ::_thesis: (x | ((y | y) | z)) | z = z | (y | x)
 (z | z) | ((y | y) | z) = z by Th121;
hence  (x | ((y | y) | z)) | z = z | (y | x) by Th100; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, y being Element of L holds x | ((y | x) | x) = y | x
let x, y be Element of L; ::_thesis: x | ((y | x) | x) = y | x
 ((x | (y | y)) | (x | (y | y))) | (y | x) = (y | x) | x by Th122;
hence  x | ((y | x) | x) = y | x by Th108; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for z, y, x being Element of L holds y = (((x | x) | x) | y) | ((z | z) | y)
now__::_thesis:_for_x,_y,_z,_p_being_Element_of_L_holds_y_=_(((x_|_x)_|_x)_|_y)_|_((z_|_z)_|_y)
let x, y, z, p be Element of L; ::_thesis: y = (((x | x) | x) | y) | ((z | z) | y)
 (y | (((p | (p | p)) | (p | (p | p))) | z)) | (y | (((p | (p | p)) | (p | (p | p))) | z)) = y by Th124;
hence  y = (((x | x) | x) | y) | ((z | z) | y) by Th110; ::_thesis: verum
end;
hence  for z, y, x being Element of L holds y = (((x | x) | x) | y) | ((z | z) | y) ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for z, y being Element of L holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y
now__::_thesis:_for_z,_y,_x_being_Element_of_L_holds_(y_|_((y_|_y)_|_z))_|_(y_|_((y_|_y)_|_z))_=_y
let z, y, x be Element of L; ::_thesis: (y | ((y | y) | z)) | (y | ((y | y) | z)) = y
 (((x | x) | x) | y) | ((z | z) | y) = y by Th127;
hence  (y | ((y | y) | z)) | (y | ((y | y) | z)) = y by Th114; ::_thesis: verum
end;
hence  for z, y being Element of L holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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
let x, z, y be Element of L; ::_thesis: (((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z)) = ((x | x) | ((y | y) | z)) | z
 (z | ((z | z) | y)) | (z | ((z | z) | y)) = z by Th128;
hence  (((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z)) = ((x | x) | ((y | y) | z)) | z by Th117; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, z, y being Element of L holds (((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z)) = z | (y | (x | x))
let x, z, y be Element of L; ::_thesis: (((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z)) = z | (y | (x | x))
 ((x | x) | ((y | y) | z)) | z = z | (y | (x | x)) by Th125;
hence  (((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z)) = z | (y | (x | x)) by Th129; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for y, x being Element of L holds ((x | y) | (x | y)) | x = x | y
let y, x be Element of L; ::_thesis: ((x | y) | (x | y)) | x = x | y
 (x | (y | y)) | (x | y) = x by Th109;
hence  ((x | y) | (x | y)) | x = x | y by Th121; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, w being Element of L holds (w | w) | (w | p) = w
let p, w be Element of L; ::_thesis: (w | w) | (w | p) = w
 p | w = w | p by Th83;
hence  (w | w) | (w | p) = w by Th121; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, p being Element of L holds (p | w) | (w | w) = w
let w, p be Element of L; ::_thesis: (p | w) | (w | w) = w
 (w | w) | (p | w) = (p | w) | (w | w) by Th83;
hence  (p | w) | (w | w) = w by Th121; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, y, w being Element of L holds (w | (y | (y | y))) | (w | p) = w
let p, y, w be Element of L; ::_thesis: (w | (y | (y | y))) | (w | p) = w
 w | w = w | (y | (y | y)) by SHEFFER1:def_14;
hence  (w | (y | (y | y))) | (w | p) = w by Th132; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for p, w being Element of L holds (w | p) | (w | w) = w
let p, w be Element of L; ::_thesis: (w | p) | (w | w) = w
 (w | w) | (w | p) = (w | p) | (w | w) by Th83;
hence  (w | p) | (w | w) = w by Th132; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for y, p, w being Element of L holds (w | p) | (w | (y | (y | y))) = w
let y, p, w be Element of L; ::_thesis: (w | p) | (w | (y | (y | y))) = w
 w | w = w | (y | (y | y)) by SHEFFER1:def_14;
hence  (w | p) | (w | (y | (y | y))) = w by Th135; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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)))
let p, q, w, y, x be Element of L; ::_thesis: (((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)))
 (w | (x | q)) | (w | (x | q)) = ((x | (y | (y | y))) | w) | ((q | q) | w) by Th73;
hence  (((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))) by Th73; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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)))
now__::_thesis:_for_y,_p,_w,_q,_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)))
let y, p, w, q, x be Element of L; ::_thesis: (((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q))) = w | (((x | q) | (x | q)) | (w | (x | q)))
 (w | (p | (p | p))) | (w | (x | q)) = w by Th134;
hence  (((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q))) = w | (((x | q) | (x | q)) | (w | (x | q))) by Th137; ::_thesis: verum
end;
hence  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))) ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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)
let q, w, y, x be Element of L; ::_thesis: (((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q))) = w | (x | q)
 ((x | q) | (x | q)) | (w | (x | q)) = x | q by Th121;
hence  (((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q))) = w | (x | q) by Th138; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let z, p, q, y, x be Element of L; ::_thesis: (((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))
 ((x | (y | (y | y))) | q) | ((z | z) | q) = (q | (x | z)) | (q | (x | z)) by Th73;
hence  (((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)) by Th73; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let z, p, q, y, x be Element of L; ::_thesis: q | (x | z) = (((z | z) | (p | (p | p))) | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q))
 (((x | (y | (y | y))) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z))) = q | (x | z) by Th139;
hence  q | (x | z) = (((z | z) | (p | (p | p))) | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q)) by Th140; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
now__::_thesis:_for_p,_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))
let p, z, q, y, x be Element of L; ::_thesis: q | (x | z) = (z | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q))
 (z | z) | (p | (p | p)) = z by Th71;
hence  q | (x | z) = (z | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q)) by Th141; ::_thesis: verum
end;
hence  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)) ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for v, p, y, x being Element of L holds p | (x | v) = (v | ((x | (y | (y | y))) | p)) | p
let v, p, y, x be Element of L; ::_thesis: p | (x | v) = (v | ((x | (y | (y | y))) | p)) | p
 (p | p) | ((x | (y | (y | y))) | p) = p by Th121;
hence  p | (x | v) = (v | ((x | (y | (y | y))) | p)) | p by Th142; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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)
let y, w, z, v, x be Element of L; ::_thesis: (w | (z | (x | v))) | (((x | (y | (y | y))) | z) | ((v | v) | z)) = z | (x | v)
 (z | (x | v)) | (z | (x | v)) = ((x | (y | (y | y))) | z) | ((v | v) | z) by Th73;
hence  (w | (z | (x | v))) | (((x | (y | (y | y))) | z) | ((v | v) | z)) = z | (x | v) by Th133; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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)
let y, z, x be Element of L; ::_thesis: ((y | ((x | x) | z)) | (y | ((x | x) | z))) | ((x | y) | ((z | z) | y)) = y | ((x | x) | z)
 (y | ((x | x) | z)) | (y | ((x | x) | z)) = (x | y) | ((z | z) | y) by Th74;
hence  ((y | ((x | x) | z)) | (y | ((x | x) | z))) | ((x | y) | ((z | z) | y)) = y | ((x | x) | z) by Th121; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for z, y, x being Element of L holds (z | (x | y)) | y = y | ((x | x) | z)
let z, y, x be Element of L; ::_thesis: (z | (x | y)) | y = y | ((x | x) | z)
 ((y | ((x | x) | z)) | (y | ((x | x) | z))) | ((x | y) | ((z | z) | y)) = (z | (x | y)) | y by Th123;
hence  (z | (x | y)) | y = y | ((x | x) | z) by Th145; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, w, y, z being Element of L holds (((x | x) | w) | ((z | (y | (y | y))) | w)) | w = w | (x | z)
let x, w, y, z be Element of L; ::_thesis: (((x | x) | w) | ((z | (y | (y | y))) | w)) | w = w | (x | z)
 (w | (x | z)) | (w | (x | z)) = ((x | x) | w) | ((z | (y | (y | y))) | w) by Th75;
hence  (((x | x) | w) | ((z | (y | (y | y))) | w)) | w = w | (x | z) by Th131; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for z, w, x being Element of L holds w | (z | ((x | x) | w)) = w | (x | z)
now__::_thesis:_for_x,_w,_p,_z_being_Element_of_L_holds_w_|_(z_|_((x_|_x)_|_w))_=_w_|_(x_|_z)
let x, w, p, z be Element of L; ::_thesis: w | (z | ((x | x) | w)) = w | (x | z)
 (((x | x) | w) | ((z | (p | (p | p))) | w)) | w = w | (z | ((x | x) | w)) by Th143;
hence  w | (z | ((x | x) | w)) = w | (x | z) by Th147; ::_thesis: verum
end;
hence  for z, w, x being Element of L holds w | (z | ((x | x) | w)) = w | (x | z) ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let p, z, y, x be Element of L; ::_thesis: ((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))
 ((x | (y | (y | y))) | z) | ((p | p) | z) = (z | (x | p)) | (z | (x | p)) by Th73;
hence  ((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)) by Th87; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))
let p, z, y, x be Element of L; ::_thesis: z | (x | p) = (((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z))
 ((z | (x | p)) | (z | (x | p))) | (((x | (y | (y | y))) | z) | ((p | p) | z)) = z | (x | p) by Th144;
hence  z | (x | p) = (((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z)) by Th149; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for z, p, y, x being Element of L holds z | (x | p) = z | (p | ((x | (y | (y | y))) | (x | (y | (y | y)))))
let z, p, y, x be Element of L; ::_thesis: z | (x | p) = z | (p | ((x | (y | (y | y))) | (x | (y | (y | y)))))
 (((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z)) = z | (p | ((x | (y | (y | y))) | (x | (y | (y | y))))) by Th130;
hence  z | (x | p) = z | (p | ((x | (y | (y | y))) | (x | (y | (y | y))))) by Th150; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for z, p, x being Element of L holds z | (x | p) = z | (p | x)
now__::_thesis:_for_y,_z,_p,_x_being_Element_of_L_holds_z_|_(x_|_p)_=_z_|_(p_|_x)
let y, z, p, x be Element of L; ::_thesis: z | (x | p) = z | (p | x)
 (x | (y | (y | y))) | (x | (y | (y | y))) = x by Th136;
hence  z | (x | p) = z | (p | x) by Th151; ::_thesis: verum
end;
hence  for z, p, x being Element of L holds z | (x | p) = z | (p | x) ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, q, p being Element of L holds (p | q) | w = w | (q | p)
let w, q, p be Element of L; ::_thesis: (p | q) | w = w | (q | p)
 w | (p | q) = (p | q) | w by Th83;
hence  (p | q) | w = w | (q | p) by Th152; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, p, q being Element of L holds ((q | p) | w) | q = q | ((p | p) | w)
let w, p, q be Element of L; ::_thesis: ((q | p) | w) | q = q | ((p | p) | w)
 w | (p | q) = (q | p) | w by Th153;
hence  ((q | p) | w) | q = q | ((p | p) | w) by Th146; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for z, w, y, x being Element of L holds w | x = w | ((x | z) | (((x | (y | (y | y))) | (x | (y | (y | y)))) | w))
let z, w, y, x be Element of L; ::_thesis: w | x = w | ((x | z) | (((x | (y | (y | y))) | (x | (y | (y | y)))) | w))
 (x | (y | (y | y))) | (x | z) = x by Th134;
hence  w | x = w | ((x | z) | (((x | (y | (y | y))) | (x | (y | (y | y)))) | w)) by Th148; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for w, z, x being Element of L holds w | x = w | ((x | z) | (x | w))
now__::_thesis:_for_y,_w,_z,_x_being_Element_of_L_holds_w_|_x_=_w_|_((x_|_z)_|_(x_|_w))
let y, w, z, x be Element of L; ::_thesis: w | x = w | ((x | z) | (x | w))
 (x | (y | (y | y))) | (x | (y | (y | y))) = x by Th136;
hence  w | x = w | ((x | z) | (x | w)) by Th155; ::_thesis: verum
end;
hence  for w, z, x being Element of L holds w | x = w | ((x | z) | (x | w)) ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))))
let q, x, z, y be Element of L; ::_thesis: (x | y) | (((x | (y | (z | (z | z)))) | q) | x) = (x | y) | (x | (y | (z | (z | z))))
 (x | (y | (z | (z | z)))) | (x | y) = x by Th113;
hence  (x | y) | (((x | (y | (z | (z | z)))) | q) | x) = (x | y) | (x | (y | (z | (z | z)))) by Th156; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: 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))))
let x, q, z, y be Element of L; ::_thesis: (x | y) | (x | (((y | (z | (z | z))) | (y | (z | (z | z)))) | q)) = (x | y) | (x | (y | (z | (z | z))))
 ((x | (y | (z | (z | z)))) | q) | x = x | (((y | (z | (z | z))) | (y | (z | (z | z)))) | q) by Th154;
hence  (x | y) | (x | (((y | (z | (z | z))) | (y | (z | (z | z)))) | q)) = (x | y) | (x | (y | (z | (z | z)))) by Th157; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for z, x, q, y being Element of L holds (x | y) | (x | (y | q)) = (x | y) | (x | (y | (z | (z | z))))
let z, x, q, y be Element of L; ::_thesis: (x | y) | (x | (y | q)) = (x | y) | (x | (y | (z | (z | z))))
 (y | (z | (z | z))) | (y | (z | (z | z))) = y by Th136;
hence  (x | y) | (x | (y | q)) = (x | y) | (x | (y | (z | (z | z)))) by Th158; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: for x, q, y being Element of L holds (x | y) | (x | (y | q)) = x
now__::_thesis:_for_q,_x,_z,_y_being_Element_of_L_holds_(x_|_y)_|_(x_|_(y_|_q))_=_x
let q, x, z, y be Element of L; ::_thesis: (x | y) | (x | (y | q)) = x
 (x | y) | (x | (y | (z | (z | z)))) = x by Th112;
hence  (x | y) | (x | (y | q)) = x by Th159; ::_thesis: verum
end;
hence  for x, q, y being Element of L holds (x | y) | (x | (y | q)) = x ; ::_thesis: verum
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
let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; ::_thesis: L is satisfying_Sh_1
given a, b, c being Element of L such that A1: (a | ((b | a) | a)) | (b | (c | a)) <> b ; :: according to SHEFFER2:def_1 ::_thesis: contradiction
A2: a | ((b | a) | a) = b | a by Th126;
 not (a | ((b | a) | a)) | (b | (a | c)) = b by A1, Th83;
hence  contradiction by A2, Th160; ::_thesis: verum
end;

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;