let k, n be Element of NAT ; :: thesis: ( k in SegM n iff k <= n )
thus ( k in SegM n implies k <= n ) :: thesis: ( k <= n implies k in SegM n )

proof

assume k in SegM n ; :: thesis: k <= n
then ex i being Element of NAT st
( k = i & i <= n ) ;
hence k <= n ; :: thesis: verum

end;

thus ( k <= n implies k in SegM n ) ; :: thesis: verum