let a be Nat; :: thesis: ( a divides 1 implies a = 1 )
assume A1: a divides 1 ; :: thesis: a = 1
then a divides 1 + 1 by NAT_D:8;
hence a = 1 by A1, NEWTON:39; :: thesis: verum