for a, b, c being Nat holds
( c in seq (a,b) iff ( 1 + a <= c & c <= b + a ) )