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 )

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

proof

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

then ex i being Nat st

( k = i & i <= n ) ;

hence k <= n ; :: thesis: verum

end;then ex i being Nat st

( k = i & i <= n ) ;

hence k <= n ; :: thesis: verum