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