theorem Th69: :: SHEFFER2:69

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