let L be non empty ShefferStr ; :: thesis: ( L is trivial implies ( L is satisfying_Sheffer_1 & L is satisfying_Sheffer_2 & L is satisfying_Sheffer_3 ) )
assume A1: L is trivial ; :: thesis: ( L is satisfying_Sheffer_1 & L is satisfying_Sheffer_2 & L is satisfying_Sheffer_3 )
thus L is satisfying_Sheffer_1 :: thesis: ( L is satisfying_Sheffer_2 & L is satisfying_Sheffer_3 )

proof

let x be Element of L; :: according to SHEFFER1:def 13 :: thesis: (x | x) | (x | x) = x
thus (x | x) | (x | x) = x by A1, STRUCT_0:def 10; :: thesis: verum

end;

thus L is satisfying_Sheffer_2 :: thesis: L is satisfying_Sheffer_3

proof

let x, y be Element of L; :: according to SHEFFER1:def 14 :: thesis: x | (y | (y | y)) = x | x
thus x | (y | (y | y)) = x | x by A1, STRUCT_0:def 10; :: thesis: verum

end;

let x, y, z be Element of L; :: according to SHEFFER1:def 15 :: thesis: (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x)
thus (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) by A1, STRUCT_0:def 10; :: thesis: verum