let a, b be Nat; :: thesis: ( a in Seg b iff ( 1 <= a & a <= b ) )
( a in { m where m is Nat : ( 1 <= m & m <= b ) } iff ex m being Nat st
( a = m & 1 <= m & m <= b ) ) ;
hence ( a in Seg b iff ( 1 <= a & a <= b ) ) ; :: thesis: verum