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