theorem :: NAT_LAT:13

for p, q being Element of NatPlus_Lattice holds p "\/" q = (@ p) lcm (@ q) ;