theorem Th1: :: FINSEQ_1:1

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