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