theorem :: SHEFFER1:29

for L being non empty satisfying_Sheffer_3 ShefferOrthoLattStr
for x, y, z being Element of L holds (x | (y | z)) " = ((y ") | x) | ((z ") | x) by Def15;