let a, b be natural Number ; :: thesis: ( a in Seg b iff ( 1 <= a & a <= b ) )
A1: ( a is Nat & b is Nat ) by TARSKI:1;
( 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 ) ) by A1; :: thesis: verum