Equivalence of Formulations of Pasch's Axiom

Theorem

The two forms of Pasch's Axiom in Tarski's Geometry are consistent.

That is, the expressions:

$(1): \quad \forall a, b, c, p, q: \exists x: \mathsf B a p c \land \mathsf B b q c \implies \mathsf B p x b \land \mathsf B q x a$

and:

$(2): \quad \forall a, b, c, p, q: \exists x: \mathsf B a p c \land \mathsf B q c b \implies \mathsf B a x q \land \mathsf B b p x$

are logically equivalent.

Proof

This theorem requires a proof. In particular: It is important that we identify which other axioms this equivalence is based on for foundational purposes (and possible generalisations) You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{ProofWanted}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Sources

June 1999: Alfred Tarski and Steven Givant: Tarski's System of Geometry (Bull. Symb. Log. Vol. 5, no. 2: pp. 175 – 214) : p. $196$