theorem Th7: :: NAT_LAT:7

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