theorem Th4: :: FINSEQ_6:130

for m, n being Nat holds card { k where k is Nat : ( m <= k & k <= m + n ) } = n + 1