let k be Element of 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;

assume 1 <= k ; :: thesis: not k is zero
hence not k is zero ; :: thesis: verum