let k, n be natural number ; :: thesis: ( k < n implies k + 1 in Seg n )
assume A1: k < n ; :: thesis: k + 1 in Seg n
A2: 1 <= k + 1 by NAT_1:12;
k + 1 <= n by A1, NAT_1:13;
hence k + 1 in Seg n by A2, FINSEQ_1:3; :: thesis: verum