let i, n be Nat; :: thesis: ( i in Seg n implies i + 1 in Seg (n + 1) )

assume A1: i in Seg n ; :: thesis: i + 1 in Seg (n + 1)

then 1 <= i by FINSEQ_1:1;

then 1 + 1 <= i + 1 by XREAL_1:6;

then A2: 1 <= i + 1 by XXREAL_0:2;

i <= n by A1, FINSEQ_1:1;

then i + 1 <= n + 1 by XREAL_1:6;

hence i + 1 in Seg (n + 1) by A2, FINSEQ_1:1; :: thesis: verum

assume A1: i in Seg n ; :: thesis: i + 1 in Seg (n + 1)

then 1 <= i by FINSEQ_1:1;

then 1 + 1 <= i + 1 by XREAL_1:6;

then A2: 1 <= i + 1 by XXREAL_0:2;

i <= n by A1, FINSEQ_1:1;

then i + 1 <= n + 1 by XREAL_1:6;

hence i + 1 in Seg (n + 1) by A2, FINSEQ_1:1; :: thesis: verum