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:43
.= lcmlat . ((lcmlat . (p,q)),r) ; :: thesis: verum