let n, i be Nat; :: thesis: ( i in Seg n implies (n + 1) - i in Seg n )
assume A1: i in Seg n ; :: thesis: (n + 1) - i in Seg n
i <= n by A1, FINSEQ_1:1;
then i + 1 <= n + 1 by XREAL_1:6;
then A2: (i + 1) - i <= (n + 1) - i by XREAL_1:9;
1 <= i by A1, FINSEQ_1:1;
then n + 1 <= i + n by XREAL_1:6;
then A3: (n + 1) - i <= (i + n) - i by XREAL_1:9;
(n + 1) - i in NAT by A2, INT_1:3;
hence (n + 1) - i in Seg n by A2, A3; :: thesis: verum