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