theorem :: NAT_LAT:1

for p, q being Element of Nat_Lattice holds p "\/" q = p lcm q ;