let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; :: thesis: for y, x being Element of L holds ((x | y) | (x | y)) | x = x | y
let y, x be Element of L; :: thesis: ((x | y) | (x | y)) | x = x | y
(x | (y | y)) | (x | y) = x by Th109;
hence ((x | y) | (x | y)) | x = x | y by Th121; :: thesis: verum