let n be Nat; :: thesis: 1 in Seg (n + 1)
0 <= n by NAT_1:2;
then 0 + 1 <= n + 1 by XREAL_1:7;
hence 1 in Seg (n + 1) by FINSEQ_1:1; :: thesis: verum