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 consider i being Element of NAT such that
A1: ( k = i & m <= i & i <= n ) ;
thus ( m <= k & k <= n ) by A1; :: thesis: verum

end;

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