theorem Th73: :: NUMBER19:73

for n, m, k being Nat holds
( k in seq (n,m) iff ( n < k & k <= n + m ) )