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

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