let k be Nat; :: thesis: ( not k is zero iff 1 <= k )

hereby :: thesis: ( 1 <= k implies not k is zero )

assume not k is zero ; :: thesis: 1 <= k
then 0 + 1 <= k by NAT_1:13;
hence 1 <= k ; :: thesis: verum

end;

thus ( 1 <= k implies not k is zero ) ; :: thesis: verum