let k, n be natural Number ; :: thesis: ( k < k + n iff 1 <= n )
thus ( k < k + n implies 1 <= n ) :: thesis: ( 1 <= n implies k < k + n )
proof
assume A1: k < k + n ; :: thesis: 1 <= n
assume not 1 <= n ; :: thesis: contradiction
then n = 0 by Th14;
hence contradiction by A1; :: thesis: verum
end;
assume 1 <= n ; :: thesis: k < k + n
hence k < k + n by Th16; :: thesis: verum