theorem Th89: :: SHEFFER2:89

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