proposition: Lemma l6_3_1 : forall A B P, Out P A B -> (A<>P /\ B<>P /\ exists C, C<>P /\ Bet A P C /\ Bet B P C).
proof: Proof. unfold Out. intros. spliter. repeat split; try assumption. induction H1. assert(exists C, Bet A P C /\ P <> C) by (apply point_construction_different). ex_and H2 C. exists C. repeat split; eBetween. assert(exists C, Bet B P C /\ P <> C) by (apply point_construction_different). ex_and H2 C. exists C. repeat split;eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le