let n be Element of NAT ; :: thesis: 1 in Seg (n + 1)
0 <= n by NAT_1:2;
then 0 + 1 <= n + 1 by XREAL_1:9;
hence 1 in Seg (n + 1) by FINSEQ_1:3; :: thesis: verum