theorem Th67: :: SHEFFER2:67

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