Bounding solutions of ODE I want to prove the following lemma:

Let $x'=f(x,t)$ be a ODE and consider a derivable function $y(t)$ such that $y'(t) < f(y(t), t)$. Then if for a certain solution $x$ of the ODE and a certain $t_0$ we have that $x(t_0) \ge y(t_0)$ then we always have that $x(t) > y(t)$ for all $t > t_0$

Intuitively this seems correct to me, but the formal proof eludes me.
Is this true? Is there a simple proof?
 A: I assume that $f(x, t)$ is jointly continuous in $x$ and $t$.  This is a pretty typical assumption for such $f(x, t)$ in the context of ordinary differential equations.
We observe that the above assumption implies that $x(t)$ and $y(t)$ are both continuous.  This follows from the fact that they are both differentiable, $x(t)$ because it satisfies 
$x'(t) = f(x(t), t), \tag 1$
and $y(t)$ by hypothesis--it is given differentiable, and this implies continuity.
We are given that 
$y(t_0) \le x(t_0) \tag 2$
and that
$y'(t) < f(y(t), t); \tag 3$
if now
$y(t_0) < x(t_0), \tag 4$
then by the continuity of $x(t)$, $y(t)$ we see that there is some $t_1  > t_0$ such that
$y(t) < x(t), \tag 5$
for $t \in [t_0, t_1]$.  In particular,
$y(t_1) < x(t_1); \tag 6$
if, on the other hand,
$y(t_0) = x(t_0), \tag 7$
then we may write
$x(t) - y(t) = (x(t_0) - y(t_0)) + \displaystyle \int_{t_0}^t (x'(s) - y'(s)) ds = \int_{t_0}^t (x'(s) - y'(s)) ds; \tag 8$
now, at $t = t_0$ we have
$y'(t_0) < f(y(t_0), t_0) = f(x(t_0), t_0) = x'(t_0); \tag 9$
again by the continuity of $x'(t)$, $y'(t)$ we may select $t_1$ sufficiently small that
$x'(t) - y'(t) > 0, \; t \in [t_0, t_1], \tag{10}$
and this implies via (8) that
$x(t) - y(t) = \displaystyle \int_{t_0}^t (x'(s) - y'(s)) ds > 0, \tag{11}$
and hence
$y(t) < x(t) \; \text{for} \; t \in (0, t_1], \tag{12}$
whence in particular
$y(t_1) < x(t_1). \tag{13}$
We have now established that, under the given hypothesis, there is a $t_1 > t_0$ such that
$x(t) > y(t) \; t \in (t_0, t_1]. \tag{14}$
Next we assume that, for some $t > t_1$,
$y(t) = x(t); \tag{15}$
given that such $t$ exists, we let $\tau$ be the least $t$ satisfying (15).  By (14), $\tau > t_1$; since
$y(\tau) = x(\tau), \tag{16}$
we may affirm that
$y'(\tau) < f(y(\tau), \tau) = f(x(\tau), \tau) = x'(\tau); \tag{17}$
and again by continuity we may find some $\epsilon > 0$ such that
$y'(t) < x'(t) \; \text{for} \; t \in [\tau - \epsilon, \tau]. \tag{18}$
Noting that
$y(\tau - \epsilon) < x(\tau - \epsilon), \tag{19}$
we may apply (8), replacing $t_0$ with $\tau - \epsilon$ and $t$ with $\tau$:
$x(\tau) - y(\tau)$
$= (x(\tau - \epsilon) - y(\tau - \epsilon)) + \displaystyle \int_{\tau - \epsilon}^\tau (x'(s) - y'(s)) ds > x(\tau - \epsilon) - y(\tau - \epsilon) > 0 \tag{20}$
by virtue of (18), in contradiction to (16); thus no $\tau > t_1$ such that (16) binds exists.  We have thus shown that $x(t) > y(t)$ for all $t > t_0$.
A: Let $t_*>t_0$ be the point of the first intersection of $y=y(t)$ and $x=x(t)$:

We have $x(t_*)=y(t_*)$;
$y(t)$ is below $x(t)$, thus, $\dot y(t_*)\ge \dot x(t_*)=f(x(t_*),t)=f(y(t_*),t)$. It contradicts with the condition $\dot y(t)<f(y(t),t)$, therefore, $y=y(t)$ and $x=x(t)$ do not intersect.
