theorem Th144: :: SHEFFER2:144

for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
for y, w, z, v, x being Element of L holds (w | (z | (x | v))) | (((x | (y | (y | y))) | z) | ((v | v) | z)) = z | (x | v)