I'm trying to prove the following result in neutral geometry from Hilbert's axioms:
Given a circle centered at $o$ and the point $p$ lying outside the circle there exists a line passing through $p$ tangent to the circle.
My idea of the proof is to use the following theorem which is a consequence of Dedekind's axiom:
Assume we are given a half-pencil $\mathfrak{P}$ (the set of all halflines with the same origin $p$ contained in some halfplane $M$ where $p$ lies on the boundary $L$ of $M$) ordered by relation $<$ defined: $H_1<H_2$ iff $B(AH_1H_2)$, where $A$ is one of the halflines contained in $L$ with the origin $p$. Assume $\mathfrak{P}$ is divided into two non-empty, disjoint sets $\mathfrak{X},\mathfrak{Y}$ such that $\mathfrak{X}\cup \mathfrak{Y}=\mathfrak{P}$ and moreover $X<Y$ for all $X\in\mathfrak{X},Y\in\mathfrak{Y}$. Then there exists a halfline $T\in\mathfrak{P}$ such that $X<T$ implies $X\in\mathfrak{X}$ and $T<Y$ implies $Y\in\mathfrak{Y}$.
As for the actual proof:
Let $L:=\overleftrightarrow{op}$ and $M$ be one of the halfplanes with boundary $M$ and let $\mathfrak{P}$ be a half-pencil with the origin $p$ and halfplane $M$, ordered with halfline $\overrightarrow{po}$ chosen as "first". Let $\mathfrak{X}\subset\mathfrak{P}$ be the set of all halflines which have at least one point in common with the circle and $\mathfrak{Y}\subset\mathfrak{P}$ be the rest of halflines (i.e. having no point in common with the circle). I managed to verify the assumptions of Dedekind's theorem. Therefore we have a halfline $T\in\mathfrak{P}$ such that $X<T$ implies $X\in\mathfrak{X}$ and $T<Y$ implies $Y\in\mathfrak{Y}$. Now the task is to show that $T$ is tangent in two steps which I don't know how to do:
Show that $T\in\mathfrak{X}$. To do this I assume $T\in\mathfrak{Y}$ and try to derive contradiction. I want to show that there exists a halfline $R\in\mathfrak{P}$ disjoint with the circle such that $R<T$.
Show that $T$ has exactly one point in common with the circle. To do this I assume it has two points in common and I want to show that there exists a halfline $R\in\mathfrak{P}$ not disjoint with the circle such that $T<R$.
To summarize, I need these two results:
Given a circle centered at $o$, the point $p$ lying outside the circle and the halfline $T$ with origin $p$ disjoint with the circle (and not contained in line $\overleftrightarrow{op}$), there exists a halfline $R$ with origin $p$ such that $R$ lies between $T$ and $\overrightarrow{po}$ and $R$ is as well disjoint with the circle.
Given a circle centered at $o$, the point $p$ lying outside the circle and the halfline $T$ with origin $p$ cutting the circle in two distinct points (and not contained in line $\overleftrightarrow{op}$), there exists a halfline $R$ with origin $p$ such that $T$ lies between $R$ and $\overrightarrow{po}$ and $R$ as well cuts the circle.