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