proposition: Lemma ts2__ex_bet2 : forall A B C D, TS A C B D -> TS B D A C -> exists X, Bet A X C /\ Bet B X D.
proof: Proof. intros A B C D HTS HTS'. destruct HTS as [HNCol [HNCol1 [X [HCol HBet]]]]. exists X; split; trivial. apply col_two_sides_bet with B; trivial. assert_diffs. apply invert_two_sides, col_two_sides with D; Col. intro; subst X; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar