Checking a proof of the two forms of Pasch's axiom - is the logic correct? I am seeking feedback on whether this proof is valid. In particular, in the last line, we use a kind of logic that I am unclear about:
The following are two equivalent forms of Pasch's Axiom:
F1: A line containing the vertex of a triangle and a pt. interior to the triangle intersects the opposite side of the triangle.
F2: A line intersecting one side of a triangle and an interior pt., but no vertex of the triangle, intersects one of the other 2 sides.
Proof that if F2 is true, then F1 is true:
Assume that line l intersects vertex A of triangle ABC and pt. D in the interior of the triangle. Extend side AB to pt E in direction of A. BEC is triangle and line l intersects BE (at A) and interior pt. D. By F2, line l also intersects either BC or EC. Similarly, extend side AC in direction of A to pt. F. By F2, l must intersect FB or BC. Since both conclusions are true, l must intersect BC. QED
Is the logic correct that, since l must intersect BC or EC and FB or BC, then it must intersect BC? Why can't it intersect FB and EC? The pic is clear, but this is geometry and we cannot go by the picture. Thank you for any feedback.
 A: We may formalize your your argument at the end that our line $l$ must intersect $(BC \vee EC) \wedge (FB \vee BC)$. Assuming that it is impossible to intersect both $FB$ and $EC$ then yes, it follows that the line must intersect $BC$. This can be done using a truth table argument or a reduction to cases. I will elaborate a bit more formally the second technique.
We know that both of the collections $\{BC, EC\}$ and $\{FB, BC\}$ must contain at least one edge which intersects $l$. If $l$ intersects $BC$ then we are done. Assume for the sake of contradiction that $l$ does not intersect $BC$. We know $l$ must intersect one element from each collection
$$\{BC,EC\}-\{BC\}=\{EC\}, \quad \{FB, BC\}-\{BC\}=\{FB\}$$ and hence $l$ must intersect both $EC, FB$. We have assumed this is impossible hence we have reached a contradiction.
Now if we wanted to be even more formal we would have to prove why intersecting both $EC,FB$ is impossible. This can be done by noticing that if $l$ intersects $EC,FB$ at two points that are not $A$ then these three points form a nonempty triangle and hence cannot actually form a line. I will leave it to you to formalize this argument. When doing a proof like this what counts as a "needed to justify" and "not needed to justify" is a subtle distinction so it is in general good to ere on the side of justifying more when possible.
