Crossbar Theorem
Seriously non-compliant. Thought this was going to be straightforward, but it turns out to rely upon axioms of modern geometry which are so far undocumented on $\mathsf{Pr} \infty \mathsf{fWiki}$, or at least in the form required for the folllowing to be understood.
It may also need to be brought up to our standard house style.
If you have done this or know it has been done, please remove {{Tidy}} from the code.
Theorem
Let $\triangle ABC$ be a triangle.
Let $D$ be a point in the interior of $\triangle ABC$.
Then there exists a point $E$ such that $E$ lies on both $AD$ and $BC$.
Proof
Aiming for a contradiction, suppose $BC$ does not meet ray $\overrightarrow {AD}$.
Either $BC$ meets line $\overleftrightarrow {AD}$ or it does not.
If it meets $\overleftrightarrow {AD}$, by the Line Separation Property it must meet the ray opposite to $\overrightarrow {AD}$ at a point $E \ne A$.
According to Proposition 3.8 (b), $E$ is not in the interior of $\angle CAB$.
Point $B$ does not lie on $\overleftrightarrow {AD}$; this is because $D \in \operatorname {int} \angle CAB$, so $D$ and $C$ lie on the same side of $\overleftrightarrow {AB}$, so $D \notin \set {\overleftrightarrow {AB} }$, so $B \notin \set {\overleftrightarrow {AB} }$.
Thus, since $E \in \set {\overleftrightarrow {AD} }$, we have $E \ne B$.
By the same reasoning with $C$ and $B$ interchanged, we have $E \ne C$.
Since $E \in BC$ and $E$ is not an endpoint, we have $B ∗ E ∗ C$.
Thus by Proposition 3.7, $E$ is in the interior of $\angle CAB$, which is a contradiction.
Thus $\overleftrightarrow {AD}$ does not meet $BC$ at all; that is, $B$ and $C$ are on the same side of $\overleftrightarrow {AD}$.
By B-2, we have a point $E$ such that $C ∗ A ∗ E$.
By Lemma 3.2.2, $C$ and $E$ are on opposite sides of $\overleftrightarrow {AD}$.
Thus, by B-4(iii), E and B are on opposite sides of $\overleftrightarrow {AD}$.
But by Proposition 3.8(c), $B$ is on the interior of $\angle DAE$, so $E$ and $B$ are on the same side of $\overleftrightarrow {AD}$
This is a contradiction.
Thus $\overrightarrow {AD}$ meets $BC$.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.
To discuss this in more detail, feel free to use the talk page.
Once you have done so, you can remove this instance of {{MissingLinks}} from the code.
