let L be 1 -element ShefferStr ; :: 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 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 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 STRUCT_0:def 10; :: thesis: verum