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