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