let n, k be 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 Nat st
( k = i & i <= n ) ;
hence k <= n ; :: thesis: verum

end;

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