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)