let L be non empty satisfying_Sh_1 ShefferStr ; :: thesis: for x, y being Element of L holds ((x | y) | (x | y)) | y = x | y
let x, y be Element of L; :: thesis: ((x | y) | (x | y)) | y = x | y
(y | y) | (x | y) = y by Th11;
hence ((x | y) | (x | y)) | y = x | y by Th11; :: thesis: verum