let N, K be ExtNat; :: thesis: ( K < K + N iff ( 1 <= N & K <> +infty ) )

hereby :: thesis: ( 1 <= N & K <> +infty implies K < K + N )

assume A1: K < K + N ; :: thesis: ( not N < 1 & not K = +infty )
assume ( N < 1 or K = +infty ) ; :: thesis: contradiction
then ( N = 0 or K = +infty ) by Th4c;
hence contradiction by A1, XXREAL_3:4, XXREAL_3:def 2; :: thesis: verum

end;

assume A2: ( 1 <= N & K <> +infty ) ; :: thesis: K < K + N
then reconsider k = K as Nat by Th3;

per cases ( N is Nat or N = +infty ) by Th3;

suppose N is Nat ; :: thesis: K < K + N

then reconsider n = N as Nat ;
k < k + n by A2, NAT_1:19;
hence K < K + N ; :: thesis: verum

end;

suppose N = +infty ; :: thesis: K < K + N

then A3: K + N = +infty by XXREAL_3:def 2;
k in REAL by XREAL_0:def 1;
hence K < K + N by A3, XXREAL_0:9; :: thesis: verum

end;

end;