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