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