let i be Nat; :: thesis: ( i divides 0 & 1 divides i )
0 = i * 0 ;
hence i divides 0 by Def3; :: thesis: 1 divides i
i = i * 1 ;
hence 1 divides i by Def3; :: thesis: verum