:: 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;