let k be Integer; :: thesis: ( 1 <= k implies k is Nat )
assume 1 <= k ; :: thesis: k is Nat
then reconsider k = k as Element of NAT by INT_1:3;
k is Nat ;
hence k is Nat ; :: thesis: verum