:: deftheorem Def15 defines satisfying_Sheffer_3 SHEFFER1:def 15 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_3 iff for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) );