proposition: Lemma l6_3_2 : forall A B P, (A<>P /\ B<>P /\ exists C, C<>P /\ Bet A P C /\ Bet B P C) -> Out P A B.
proof: Proof. intros. spliter. ex_and H1 C. unfold Out. repeat split; try assumption; eapply l5_2; eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le