theorem Th1: :: FINSEQ_5:1

for i, n being Nat st i <= n holds
(n - i) + 1 is Element of NAT