proposition: Lemma out_bet_out_2 : forall A B C P, Out P A C -> Bet A B C -> Out P B C.
proof: Proof. intros. apply l6_6. eapply out_bet_out_1. apply l6_6. apply H. apply between_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le