let m, n, k be Nat; :: thesis: ( k in nat_interval (m,n) iff ( m <= k & k <= n ) )

hereby :: thesis: ( m <= k & k <= n implies k in nat_interval (m,n) )

assume k in nat_interval (m,n) ; :: thesis: ( m <= k & k <= n )
then ex i being Nat st
( k = i & m <= i & i <= n ) ;
hence ( m <= k & k <= n ) ; :: thesis: verum

end;

assume ( m <= k & k <= n ) ; :: thesis: k in nat_interval (m,n)
hence k in nat_interval (m,n) ; :: thesis: verum