theorem Th118: :: SHEFFER2:118

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