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

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