proposition: Lemma out_bet_out_1 : forall A B C P, Out P A C -> Bet A B C -> Out P A B.
proof: Proof. intros. induction (eq_dec_points B P). subst P. apply False_ind. apply (not_bet_and_out A B C). split; assumption. unfold Out in *. spliter. repeat split. assumption. assumption. induction H3. left. eapply between_inner_transitivity. apply H3. assumption. right. eapply between_exchange2. apply H3. apply between_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le