let n, k be natural Number ; :: thesis: ( k <> 0 implies n < n + k )
assume k <> 0 ; :: thesis: n < n + k
then A1: n <> n + k ;
n <= n + k by Th12;
hence n < n + k by A1, XXREAL_0:1; :: thesis: verum