theorem Th5: :: NAT_LAT:5

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