proposition: Lemma l6_4_1 : forall A B P, Out P A B -> Col A P B /\ ~ Bet A P B.
proof: Proof. unfold Out. intros. spliter. unfold Col. induction H1; split. Between. intro; apply H; eapply between_equality;eauto. right; left; assumption. intro; apply H0; eapply between_equality; eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le