theorem :: NAT_D:31

for i being natural Number holds i lcm i = i