:: deftheorem defines " SHEFFER1:def 16 :
for L being non empty ShefferStr
for a being Element of L holds a " = a | a;