let p, q, r be Element of Nat_Lattice ; :: thesis: 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:56
.= lcmlat . (lcmlat . p,q),r ; :: thesis: verum