for p, q, r being Element of Nat_Lattice holds
( lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (q,p)),r) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,r)),q) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,q)),p) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) )