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