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

assume L is satisfying_Sh_1 ; :: thesis: L is satisfying_Sheffer_1

then for x being Element of L holds (x | x) | (x | x) = x by Th21;

hence L is satisfying_Sheffer_1 by SHEFFER1:def 13; :: thesis: verum

assume L is satisfying_Sh_1 ; :: thesis: L is satisfying_Sheffer_1

then for x being Element of L holds (x | x) | (x | x) = x by Th21;

hence L is satisfying_Sheffer_1 by SHEFFER1:def 13; :: thesis: verum