:: SHEFFER2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

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

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

registration
cluster non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 ShefferStr ;
existence
ex 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 end;
end;

theorem Th1: :: SHEFFER2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z, u being Element of L holds ((x | (y | z)) | (x | (x | (y | z)))) | ((z | ((x | z) | z)) | (u | (x | (y | z)))) = z | ((x | z) | z)
proof end;

theorem Th2: :: SHEFFER2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | y) | (((y | ((z | y) | y)) | (x | y)) | (x | y))) | z = y | ((z | y) | y)
proof end;

theorem Th3: :: SHEFFER2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | ((x | z) | z))) = y
proof end;

theorem Th4: :: SHEFFER2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | ((x | ((x | x) | x)) | (y | (x | ((x | x) | x)))) = x | ((x | x) | x)
proof end;

theorem Th5: :: SHEFFER2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x being Element of L holds x | ((x | x) | x) = x | x
proof end;

theorem Th6: :: SHEFFER2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x being Element of L holds (x | ((x | x) | x)) | (x | x) = x
proof end;

theorem Th7: :: SHEFFER2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | x) | (x | (y | x)) = x
proof end;

theorem Th8: :: SHEFFER2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | (((y | y) | x) | x)) | y = y | y
proof end;

theorem Th9: :: SHEFFER2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds ((x | y) | (((x | y) | (x | y)) | (x | y))) | ((x | y) | (x | y)) = y | ((((x | y) | (x | y)) | y) | y)
proof end;

theorem Th10: :: SHEFFER2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | ((((y | x) | (y | x)) | x) | x) = y | x
proof end;

theorem Th11: :: SHEFFER2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | x) | (y | x) = x
proof end;

theorem Th12: :: SHEFFER2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | (y | (x | x)) = x | x
proof end;

theorem Th13: :: SHEFFER2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds ((x | y) | (x | y)) | y = x | y
proof end;

theorem Th14: :: SHEFFER2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | ((y | x) | x) = y | x
proof end;

theorem Th15: :: SHEFFER2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | y) | (x | (z | y)) = x
proof end;

theorem Th16: :: SHEFFER2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | z)) | (x | z) = x
proof end;

theorem Th17: :: SHEFFER2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((x | y) | (z | y)) = x | y
proof end;

theorem Th18: :: SHEFFER2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | (y | z)) | z) | x = x | (y | z)
proof end;

theorem Th19: :: SHEFFER2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | ((y | x) | x) = x | y
proof end;

theorem Th20: :: SHEFFER2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | y = y | x
proof end;

theorem Th21: :: SHEFFER2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | y) | (x | x) = x
proof end;

theorem Th22: :: SHEFFER2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | y) | (y | (z | x)) = y
proof end;

theorem Th23: :: SHEFFER2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | z)) | (z | x) = x
proof end;

theorem Th24: :: SHEFFER2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | y) | (y | (x | z)) = y
proof end;

theorem Th25: :: SHEFFER2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | z)) | (y | x) = x
proof end;

theorem Th26: :: SHEFFER2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | y) | (x | z)) | z = x | z
proof end;

theorem Th27: :: SHEFFER2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (x | (y | z))) = x | (y | z)
proof end;

theorem Th28: :: SHEFFER2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (x | z)
proof end;

theorem Th29: :: SHEFFER2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z, u being Element of L holds (x | (y | z)) | (x | (u | (y | x))) = (x | (y | z)) | (y | x)
proof end;

theorem Th30: :: SHEFFER2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (z | x)
proof end;

theorem Th31: :: SHEFFER2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z, u being Element of L holds (x | (y | z)) | (x | (u | (y | x))) = x
proof end;

theorem Th32: :: SHEFFER2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | (y | (x | y)) = x | x
proof end;

theorem Th33: :: SHEFFER2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | z) = x | (z | y)
proof end;

theorem Th34: :: SHEFFER2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (x | (z | (y | x)))) = x | x
proof end;

theorem Th35: :: SHEFFER2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | z)) | ((y | x) | x) = (x | (y | z)) | (x | (y | z))
proof end;

theorem Th36: :: SHEFFER2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | (y | x)) | y = y | y
proof end;

theorem Th37: :: SHEFFER2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | y) | z = z | (y | x)
proof end;

theorem Th38: :: SHEFFER2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (z | (x | y))) = x | (y | y)
proof end;

theorem Th39: :: SHEFFER2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | y) | y) | (y | (z | x)) = (y | (z | x)) | (y | (z | x))
proof end;

theorem Th40: :: SHEFFER2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z, u being Element of L holds (x | y) | (z | u) = (u | z) | (y | x)
proof end;

theorem Th41: :: SHEFFER2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | ((y | x) | z)) = x | (y | y)
proof end;

theorem Th42: :: SHEFFER2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | (y | x) = x | (y | y)
proof end;

theorem Th43: :: SHEFFER2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds (x | y) | y = y | (x | x)
proof end;

theorem Th44: :: SHEFFER2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | (y | y) = x | (x | y)
proof end;

theorem Th45: :: SHEFFER2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | y)) = (x | (z | y)) | (x | (z | y))
proof end;

theorem Th46: :: SHEFFER2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | z)) | (x | (y | y)) = (x | (y | z)) | (x | (y | z))
proof end;

theorem Th47: :: SHEFFER2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x | y)))) = x | ((y | y) | (y | y))
proof end;

theorem Th48: :: SHEFFER2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | (y | z)) | (x | (y | z))) | (y | y) = x | (y | y)
proof end;

theorem Th49: :: SHEFFER2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x | y)))) = x | y
proof end;

theorem Th50: :: SHEFFER2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (((x | y) | (x | y)) | ((z | ((x | y) | z)) | (x | y))) | (x | x) = (z | ((x | y) | z)) | (x | x)
proof end;

theorem Th51: :: SHEFFER2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = (y | z) | (y | y)
proof end;

theorem Th52: :: SHEFFER2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = y
proof end;

theorem Th53: :: SHEFFER2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((y | ((x | z) | y)) | x) = y | ((x | z) | y)
proof end;

theorem Th54: :: SHEFFER2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((y | (y | (z | x))) | x) = y | ((x | (y | (x | z))) | y)
proof end;

theorem Th55: :: SHEFFER2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | ((y | (y | (z | x))) | x) = y | (y | (z | x))
proof end;

theorem Th56: :: SHEFFER2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z, u being Element of L holds x | (y | (z | (z | (u | (y | x))))) = x | (y | y)
proof end;

theorem Th57: :: SHEFFER2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (y | (z | (x | y)))) = x | (y | (x | x))
proof end;

theorem Th58: :: SHEFFER2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (y | (z | (x | y)))) = x | x
proof end;

theorem Th59: :: SHEFFER2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y being Element of L holds x | (y | (y | y)) = x | x
proof end;

theorem Th60: :: SHEFFER2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (((y | (z | x)) | (y | (z | x))) | (z | z)) = x | (y | (z | x))
proof end;

theorem Th61: :: SHEFFER2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | (z | z)) = x | (y | (z | x))
proof end;

theorem Th62: :: SHEFFER2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds x | (y | ((z | z) | x)) = x | (y | z)
proof end;

theorem Th63: :: SHEFFER2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | ((y | y) | x))) = (x | (z | y)) | (x | (z | y))
proof end;

theorem Th64: :: SHEFFER2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | (x | (y | y)))) = (x | (z | y)) | (x | (z | y))
proof end;

theorem Th65: :: SHEFFER2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | z)) = (x | (z | y)) | (x | (z | y))
proof end;

theorem Th66: :: SHEFFER2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sh_1 ShefferStr
for x, y, z being Element of L holds ((x | x) | y) | ((z | z) | y) = (y | (x | z)) | (y | (x | z))
proof end;

theorem Th67: :: SHEFFER2:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_1
proof end;

theorem Th68: :: SHEFFER2:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_2
proof end;

theorem Th69: :: SHEFFER2:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_3
proof end;

registration
cluster non empty Lattice-like Boolean well-complemented de_Morgan properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 ShefferOrthoLattStr ;
existence
ex 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 end;
end;

registration
cluster non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 -> non empty Lattice-like Boolean ShefferOrthoLattStr ;
coherence
for 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:38;
cluster non empty Lattice-like Boolean well-complemented properly_defined -> non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ;
coherence
for 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:27, SHEFFER1:28, SHEFFER1:29;
end;

theorem Th70: :: SHEFFER2:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, w being Element of L holds w | ((x | x) | x) = w | w
proof end;

theorem Th71: :: SHEFFER2:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, x being Element of L holds x = (x | x) | (p | (p | p))
proof end;

theorem Th72: :: SHEFFER2:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds (w | w) | (w | (y | (y | y))) = w
proof end;

theorem Th73: :: SHEFFER2:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, p, y, w being Element of L holds ((w | (y | (y | y))) | p) | ((q | q) | p) = (p | (w | q)) | (p | (w | q))
proof end;

theorem Th74: :: SHEFFER2:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, p, x being Element of L holds (x | p) | ((q | q) | p) = (p | ((x | x) | q)) | (p | ((x | x) | q))
proof end;

theorem Th75: :: SHEFFER2:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p, y, q being Element of L holds ((w | w) | p) | ((q | (y | (y | y))) | p) = (p | (w | q)) | (p | (w | q))
proof end;

theorem Th76: :: SHEFFER2:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, x being Element of L holds x = (x | x) | ((p | p) | p)
proof end;

theorem Th77: :: SHEFFER2:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds (w | w) | (w | ((y | y) | y)) = w
proof end;

theorem Th78: :: SHEFFER2:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds (w | ((y | y) | y)) | (w | w) = w
proof end;

theorem Th79: :: SHEFFER2:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, y, w being Element of L holds (w | ((y | y) | y)) | (p | (p | p)) = w
proof end;

theorem Th80: :: SHEFFER2:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, x, y being Element of L holds ((y | (x | x)) | (y | (x | x))) | (p | (p | p)) = (x | x) | y
proof end;

theorem Th81: :: SHEFFER2:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y being Element of L holds y | (x | x) = (x | x) | y
proof end;

theorem Th82: :: SHEFFER2:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds w | y = ((y | y) | (y | y)) | w
proof end;

theorem Th83: :: SHEFFER2:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds w | y = y | w
proof end;

theorem Th84: :: SHEFFER2:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, p being Element of L holds (p | x) | (p | ((x | x) | (x | x))) = (((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p)
proof end;

theorem Th85: :: SHEFFER2:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, p being Element of L holds (p | x) | (p | x) = (((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p)
proof end;

theorem Th86: :: SHEFFER2:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, p being Element of L holds (p | x) | (p | x) = (x | p) | (((x | x) | (x | x)) | p)
proof end;

theorem Th87: :: SHEFFER2:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, p being Element of L holds (p | x) | (p | x) = (x | p) | (x | p)
proof end;

theorem Th88: :: SHEFFER2:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, q, w being Element of L holds ((w | q) | ((y | y) | y)) | ((w | q) | (w | q)) = ((w | w) | (w | q)) | ((q | q) | (w | q))
proof end;

theorem Th89: :: SHEFFER2:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, w being Element of L holds w | q = ((w | w) | (w | q)) | ((q | q) | (w | q))
proof end;

theorem Th90: :: SHEFFER2:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, p being Element of L holds (p | p) | (p | ((q | q) | q)) = (((q | q) | (q | q)) | p) | ((q | q) | p)
proof end;

theorem Th91: :: SHEFFER2:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, q being Element of L holds p = (((q | q) | (q | q)) | p) | ((q | q) | p)
proof end;

theorem Th92: :: SHEFFER2:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, q being Element of L holds p = (q | p) | ((q | q) | p)
proof end;

theorem Th93: :: SHEFFER2:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, w, x being Element of L holds (((x | x) | w) | ((z | z) | w)) | ((w | (x | z)) | (w | (x | z))) = ((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w | (x | z)))
proof end;

theorem Th94: :: SHEFFER2:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, w, x being Element of L holds (((x | x) | w) | ((z | z) | w)) | ((w | (x | z)) | (w | (x | z))) = w | (x | z)
proof end;

theorem Th95: :: SHEFFER2:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p being Element of L holds (p | p) | (p | (w | (w | w))) = ((w | w) | p) | (((w | w) | (w | w)) | p)
proof end;

theorem Th96: :: SHEFFER2:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds p = ((w | w) | p) | (((w | w) | (w | w)) | p)
proof end;

theorem Th97: :: SHEFFER2:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds p = ((w | w) | p) | (w | p)
proof end;

theorem Th98: :: SHEFFER2:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, q, x being Element of L holds (((x | x) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z))) = (((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q))
proof end;

theorem Th99: :: SHEFFER2:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, z, x being Element of L holds q | (x | z) = (((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q))
proof end;

theorem Th100: :: SHEFFER2:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, z, x being Element of L holds q | (x | z) = (z | ((x | x) | q)) | ((q | q) | ((x | x) | q))
proof end;

theorem Th101: :: SHEFFER2:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, y being Element of L holds w | w = ((y | y) | y) | w
proof end;

theorem Th102: :: SHEFFER2:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p being Element of L holds (p | w) | ((w | w) | p) = p
proof end;

theorem Th103: :: SHEFFER2:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds (w | w) | ((w | w) | ((y | y) | y)) = (y | y) | y
proof end;

theorem Th104: :: SHEFFER2:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w being Element of L holds (w | w) | w = (y | y) | y
proof end;

theorem Th105: :: SHEFFER2:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds (w | p) | (p | (w | w)) = p
proof end;

theorem Th106: :: SHEFFER2:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p being Element of L holds (p | (w | w)) | (w | p) = p
proof end;

theorem Th107: :: SHEFFER2:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds (w | p) | (w | (p | p)) = w
proof end;

theorem Th108: :: SHEFFER2:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y being Element of L holds y | (((y | (x | x)) | (y | (x | x))) | (x | y)) = x | y
proof end;

theorem Th109: :: SHEFFER2:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds (w | (p | p)) | (w | p) = w
proof end;

theorem Th110: :: SHEFFER2:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w, q, y being Element of L holds (((y | y) | y) | q) | ((w | w) | q) = (q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w))
proof end;

theorem Th111: :: SHEFFER2:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, w, p being Element of L holds (q | q) | ((w | w) | q) = (q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w))
proof end;

theorem Th112: :: SHEFFER2:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, y, p being Element of L holds (w | p) | (w | (p | (y | (y | y)))) = w
proof end;

theorem Th113: :: SHEFFER2:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, y, p being Element of L holds (w | (p | (y | (y | y)))) | (w | p) = w
proof end;

theorem Th114: :: SHEFFER2:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, p, y being Element of L holds (((y | y) | y) | p) | ((q | q) | p) = (p | ((p | p) | q)) | (p | ((p | p) | q))
proof end;

theorem Th115: :: SHEFFER2:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, z, x being Element of L holds ((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q)) = (((z | z) | (z | z)) | (x | q)) | ((q | q) | (x | q))
proof end;

theorem Th116: :: SHEFFER2:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, z, x being Element of L holds ((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q)) = (z | (x | q)) | ((q | q) | (x | q))
proof end;

theorem Th117: :: SHEFFER2:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, q, z being Element of L holds ((w | w) | ((z | z) | q)) | ((q | ((q | q) | z)) | (q | ((q | q) | z))) = (((z | z) | q) | (w | q)) | (((z | z) | q) | (w | q))
proof end;

theorem Th118: :: SHEFFER2:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, p, x being Element of L holds ((p | (x | p)) | (p | (x | p))) | (q | (q | q)) = (x | x) | p
proof end;

theorem Th119: :: SHEFFER2:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, x being Element of L holds p | (x | p) = (x | x) | p
proof end;

theorem Th120: :: SHEFFER2:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, y being Element of L holds (y | p) | ((y | y) | p) = (p | p) | (y | p)
proof end;

theorem Th121: :: SHEFFER2:121  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y being Element of L holds x = (x | x) | (y | x)
proof end;

theorem Th122: :: SHEFFER2:122  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y being Element of L holds (y | x) | x = ((x | (y | y)) | (x | (y | y))) | (y | x)
proof end;

theorem Th123: :: SHEFFER2:123  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, z, y being Element of L holds ((x | ((y | y) | z)) | (x | ((y | y) | z))) | ((y | x) | ((z | z) | x)) = (z | (y | x)) | x
proof end;

theorem Th124: :: SHEFFER2:124  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y, z being Element of L holds (x | (((z | (z | z)) | (z | (z | z))) | y)) | (x | (((z | (z | z)) | (z | (z | z))) | y)) = x
proof end;

theorem Th125: :: SHEFFER2:125  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, z, y being Element of L holds (x | ((y | y) | z)) | z = z | (y | x)
proof end;

theorem Th126: :: SHEFFER2:126  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, y being Element of L holds x | ((y | x) | x) = y | x
proof end;

theorem Th127: :: SHEFFER2:127  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, y, x being Element of L holds y = (((x | x) | x) | y) | ((z | z) | y)
proof end;

theorem Th128: :: SHEFFER2:128  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, y being Element of L holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y
proof end;

theorem Th129: :: SHEFFER2:129  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, z, y being Element of L holds (((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z)) = ((x | x) | ((y | y) | z)) | z
proof end;

theorem Th130: :: SHEFFER2:130  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, z, y being Element of L holds (((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z)) = z | (y | (x | x))
proof end;

theorem Th131: :: SHEFFER2:131  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, x being Element of L holds ((x | y) | (x | y)) | x = x | y
proof end;

theorem Th132: :: SHEFFER2:132  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds (w | w) | (w | p) = w
proof end;

theorem Th133: :: SHEFFER2:133  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p being Element of L holds (p | w) | (w | w) = w
proof end;

theorem Th134: :: SHEFFER2:134  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, y, w being Element of L holds (w | (y | (y | y))) | (w | p) = w
proof end;

theorem Th135: :: SHEFFER2:135  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, w being Element of L holds (w | p) | (w | w) = w
proof end;

theorem Th136: :: SHEFFER2:136  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, p, w being Element of L holds (w | p) | (w | (y | (y | y))) = w
proof end;

theorem Th137: :: SHEFFER2:137  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, q, w, y, x being Element of L holds (((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q))) = ((w | (p | (p | p))) | (w | (x | q))) | (((x | q) | (x | q)) | (w | (x | q)))
proof end;

theorem Th138: :: SHEFFER2:138  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, w, y, x being Element of L holds (((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q))) = w | (((x | q) | (x | q)) | (w | (x | q)))
proof end;

theorem Th139: :: SHEFFER2:139  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, w, y, x being Element of L holds (((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q))) = w | (x | q)
proof end;

theorem Th140: :: SHEFFER2:140  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, p, q, y, x being Element of L holds (((x | (y | (y | y))) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z))) = (((z | z) | (p | (p | p))) | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q))
proof end;

theorem Th141: :: SHEFFER2:141  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, p, q, y, x being Element of L holds q | (x | z) = (((z | z) | (p | (p | p))) | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q))
proof end;

theorem Th142: :: SHEFFER2:142  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, q, y, x being Element of L holds q | (x | z) = (z | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q))
proof end;

theorem Th143: :: SHEFFER2:143  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for v, p, y, x being Element of L holds p | (x | v) = (v | ((x | (y | (y | y))) | p)) | p
proof end;

theorem Th144: :: SHEFFER2:144  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w, z, v, x being Element of L holds (w | (z | (x | v))) | (((x | (y | (y | y))) | z) | ((v | v) | z)) = z | (x | v)
proof end;

theorem Th145: :: SHEFFER2:145  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, z, x being Element of L holds ((y | ((x | x) | z)) | (y | ((x | x) | z))) | ((x | y) | ((z | z) | y)) = y | ((x | x) | z)
proof end;

theorem Th146: :: SHEFFER2:146  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, y, x being Element of L holds (z | (x | y)) | y = y | ((x | x) | z)
proof end;

theorem Th147: :: SHEFFER2:147  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, w, y, z being Element of L holds (((x | x) | w) | ((z | (y | (y | y))) | w)) | w = w | (x | z)
proof end;

theorem Th148: :: SHEFFER2:148  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, w, x being Element of L holds w | (z | ((x | x) | w)) = w | (x | z)
proof end;

theorem Th149: :: SHEFFER2:149  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, z, y, x being Element of L holds ((z | (x | p)) | (z | (x | p))) | (((x | (y | (y | y))) | z) | ((p | p) | z)) = (((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z))
proof end;

theorem Th150: :: SHEFFER2:150  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for p, z, y, x being Element of L holds z | (x | p) = (((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z))
proof end;

theorem Th151: :: SHEFFER2:151  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, p, y, x being Element of L holds z | (x | p) = z | (p | ((x | (y | (y | y))) | (x | (y | (y | y)))))
proof end;

theorem Th152: :: SHEFFER2:152  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, p, x being Element of L holds z | (x | p) = z | (p | x)
proof end;

theorem Th153: :: SHEFFER2:153  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, q, p being Element of L holds (p | q) | w = w | (q | p)
proof end;

theorem Th154: :: SHEFFER2:154  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, p, q being Element of L holds ((q | p) | w) | q = q | ((p | p) | w)
proof end;

theorem Th155: :: SHEFFER2:155  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, w, y, x being Element of L holds w | x = w | ((x | z) | (((x | (y | (y | y))) | (x | (y | (y | y)))) | w))
proof end;

theorem Th156: :: SHEFFER2:156  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, z, x being Element of L holds w | x = w | ((x | z) | (x | w))
proof end;

theorem Th157: :: SHEFFER2:157  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for q, x, z, y being Element of L holds (x | y) | (((x | (y | (z | (z | z)))) | q) | x) = (x | y) | (x | (y | (z | (z | z))))
proof end;

theorem Th158: :: SHEFFER2:158  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, q, z, y being Element of L holds (x | y) | (x | (((y | (z | (z | z))) | (y | (z | (z | z)))) | q)) = (x | y) | (x | (y | (z | (z | z))))
proof end;

theorem Th159: :: SHEFFER2:159  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for z, x, q, y being Element of L holds (x | y) | (x | (y | q)) = (x | y) | (x | (y | (z | (z | z))))
proof end;

theorem Th160: :: SHEFFER2:160  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for x, q, y being Element of L holds (x | y) | (x | (y | q)) = x
proof end;

theorem Th161: :: SHEFFER2:161  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr holds L is satisfying_Sh_1
proof end;

registration
cluster non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 -> non empty satisfying_Sh_1 ShefferStr ;
coherence
for 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 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 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 )
proof end;
cluster non empty Lattice-like Boolean well-complemented properly_defined -> non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 ShefferOrthoLattStr ;
coherence
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
proof end;
end;