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