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