proposition: Lemma inner_pasch : forall A B C P Q, Bet A P C -> Bet B Q C -> exists x, Bet P x B /\ Bet Q x A.
proof: Proof. unfold Bet; intros. intuition;subst; try (exists P;tauto); try (exists Q;tauto); exists C;tauto. Qed.
imports: GeoCoq.Axioms.tarski_axioms