let m be Nat; :: thesis: m lcm 1 = m
set M = m lcm 1;
1 divides m by NAT_D:6;
then A1: m lcm 1 divides m by NAT_D:def 4;
m divides m lcm 1 by NAT_D:def 4;
hence m lcm 1 = m by A1, NAT_D:5; :: thesis: verum