theorem Th153: :: SHEFFER2:153

for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for w, q, p being Element of L holds (p | q) | w = w | (q | p)