let L be non empty ShefferStr ; :: thesis: ( L is satisfying_Sh_1 implies L is satisfying_Sheffer_2 )
assume L is satisfying_Sh_1 ; :: thesis: L is satisfying_Sheffer_2
then for x, y being Element of L holds x | (y | (y | y)) = x | x by Th59;
hence L is satisfying_Sheffer_2 by SHEFFER1:def 14; :: thesis: verum