let L be non empty satisfying_DN_1 ComplLLattStr ; :: 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)
(y + x) + (y + z) = z + (y + x) by Th53;
hence x + (y + z) = z + (y + x) by Th53; :: thesis: verum