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