proposition: Lemma l6_7 : forall P A B C, Out P A B -> Out P B C -> Out P A C.
proof: Proof. unfold Out. intros. spliter. repeat split; try assumption. induction H4; induction H2. left; eapply between_exchange4; eauto. eapply l5_3; eauto. eapply (l5_1 P B); auto. right; eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le