let i, n be Nat; :: thesis: ( i in Seg n implies (n -' i) + 1 in Seg n )
assume i in Seg n ; :: thesis: (n -' i) + 1 in Seg n
then A1: ( 1 <= i & i <= n ) by FINSEQ_1:3;
then n - i <= n - 1 by XREAL_1:15;
then (n - i) + 1 <= n by XREAL_1:21;
then A2: (n -' i) + 1 <= n by A1, XREAL_1:235;
1 <= (n -' i) + 1 by NAT_1:11;
hence (n -' i) + 1 in Seg n by A2, FINSEQ_1:3; :: thesis: verum