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