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