let a, b, c be Nat; :: thesis: ( c in seq (a,b) iff ( 1 + a <= c & c <= b + a ) )
A1: ( c in { m where m is Element of NAT : ( 1 + a <= m & m <= b + a ) } iff ex m being Element of NAT st
( c = m & 1 + a <= m & m <= b + a ) ) ;
c is Element of NAT by ORDINAL1:def 12;
hence ( c in seq (a,b) iff ( 1 + a <= c & c <= b + a ) ) by A1; :: thesis: verum