let m, n, k be Element of 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 Element of 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