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

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