:: deftheorem Def13 defines satisfying_Sheffer_1 SHEFFER1:def 13 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_1 iff for x being Element of L holds (x | x) | (x | x) = x );