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

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