let i be Nat; :: thesis: i lcm i = i
for m being Nat st i divides m & i divides m holds
i divides m ;
hence i lcm i = i by Def4; :: thesis: verum