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))