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