theorem Th131: :: SHEFFER2:131

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