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