let c, a, b be natural number ; :: 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 13;
hence ( c in seq a,b iff ( 1 + a <= c & c <= b + a ) ) by A1; :: thesis: verum