theorem Th161: :: SHEFFER2:161

for L being non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr holds L is satisfying_Sh_1