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