Solutions tending to infinity in finite time both forwards and backwards Is my solution correct for the part underlined in green?

$$x(t)=\frac{\tan(t)+x_0}{1-x_0\tan (t)}$$ so solutions go to infinity at:
$$\tan(t)=\frac{1}{x_0}$$

Where $t_2<0<t_1$
 A: $$
\frac{dx}{dt} =\dot{x} = 1+x^2
$$
$$
\frac{dx}{1+x^2} = dt
$$
$$
\arctan x = t+C
$$
$$
x = \tan(t+C) = \frac{\tan t + \tan C}{1-\tan t\tan C}. \tag 1
$$
When $t=0$, this is $\tan C$, so $C=\arctan x_0$.  (We could take $C$ to be $\arctan(x_0)+n\pi$ for any integer $n$, but $(1)$ would still be the same.  If some non-rigorousness is thought to afflict the steps culminating in $(1)$, one can check the solution by substitution.
This function has vertical asymptotes at
$$
\begin{cases}
\arctan\dfrac{1}{x_0} = \dfrac\pi2 - \arctan x_0\text{ and } \arctan\left(\dfrac{1}{x_0}\right) - \pi = \arctan(x_0)-\dfrac\pi 2  & \text{if }x_0>0, \\[8pt]
\arctan\dfrac{1}{x_0 }=-\dfrac\pi2-\arctan x_0\text{ and } \arctan\left(\dfrac{1}{x_0}\right) + \pi = -\arctan(x_0)+ \dfrac\pi 2 & \text{if }x_0<0, \\[8pt]
\pm\dfrac\pi2 & \text{if } x_0=0.
\end{cases}
$$
The solution is unique on the interval between these two asymptotes. It is not unique on adjacent intervals, but that is probably not of interest for contemplated applications.
How would one prove uniqueness.  Instantly I think of the mean value theorem, but then of the non-linearity of the equation.   However, the steps leading to $(1)$ can be reworked into a rigorous proof of uniqueness by citing the chain rule in the right places.
