:: deftheorem Def1 defines satisfying_Sh_1 SHEFFER2:def 1 :
for L being non empty ShefferStr holds
( L is satisfying_Sh_1 iff for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | x)) = y );