for N, K being ExtNat holds
( K < K + N iff ( 1 <= N & K <> +infty ) )