let L be non empty ShefferStr ; :: thesis: ( L is satisfying_Sh_1 implies L is satisfying_Sheffer_3 )

assume L is satisfying_Sh_1 ; :: thesis: L is satisfying_Sheffer_3

then for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) by Th66;

hence L is satisfying_Sheffer_3 by SHEFFER1:def 15; :: thesis: verum

assume L is satisfying_Sh_1 ; :: thesis: L is satisfying_Sheffer_3

then for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) by Th66;

hence L is satisfying_Sheffer_3 by SHEFFER1:def 15; :: thesis: verum