let L be non empty ShefferStr ; :: thesis: ( L is trivial implies L is satisfying_Sh_1 )
assume L is trivial ; :: thesis: L is satisfying_Sh_1
then for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | x)) = y by STRUCT_0:def 10;
hence L is satisfying_Sh_1 by Def1; :: thesis: verum