for L being non empty ShefferStr st L is satisfying_Sh_1 holds
L is satisfying_Sheffer_1