:: deftheorem Def2 defines lcm NEWTON03:def 4 :
for a, b being Integer holds a lcm b = |.a.| lcm |.b.|;