let p,

q,

r be

Element of

Nat_Lattice;

lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,q)),r)
set s =

q "\/" r;

thus lcmlat . (

p,

(lcmlat . (q,r))) =

p "\/" (q "\/" r)
.=

(p "\/" q) "\/" r
by NEWTON:43
.=

lcmlat . (

(lcmlat . (p,q)),

r)
;

verum