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