let i be natural Number ; :: thesis: i lcm i = i
A0: i is Nat by TARSKI:1;
for m being Nat st i divides m & i divides m holds
i divides m ;
hence i lcm i = i by A0, Def4; :: thesis: verum