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