for a, b being natural Number holds
( a in Seg b iff ( 1 <= a & a <= b ) )