let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; :: thesis: L is satisfying_Sh_1
given a, b, c being Element of L such that A1: (a | ((b | a) | a)) | (b | (c | a)) <> b ; :: according to SHEFFER2:def 1 :: thesis: contradiction
A2: a | ((b | a) | a) = b | a by Th126;
not (a | ((b | a) | a)) | (b | (a | c)) = b by A1, Th83;
hence contradiction by A2, Th160; :: thesis: verum