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;