proposition: Lemma fourth_point : forall A B C P, A <> B -> B <> C -> Col A B P -> Bet A B C -> Bet P A B \/ Bet A P B \/ Bet B P C \/ Bet B C P.
proof: Proof. intros. induction H1. assert(HH:= l5_2 A B C P H H2 H1). right; right. induction HH. right; auto. left; auto. induction H1. right; left. Between. left; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col