let i, n be Nat; :: thesis: ( i in Seg n implies (n -' i) + 1 in Seg n )
A1: 1 <= (n -' i) + 1 by NAT_1:11;
assume A2: i in Seg n ; :: thesis: (n -' i) + 1 in Seg n
then 1 <= i by FINSEQ_1:1;
then n - i <= n - 1 by XREAL_1:13;
then A3: (n - i) + 1 <= n by XREAL_1:19;
i <= n by A2, FINSEQ_1:1;
then (n -' i) + 1 <= n by A3, XREAL_1:233;
hence (n -' i) + 1 in Seg n by A1, FINSEQ_1:1; :: thesis: verum