let k be Element of NAT ; :: thesis: ( not k is empty iff 1 <= k )

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

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

end;

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