theorem Th154: :: SHEFFER2:154

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)