proposition: Lemma out_suppa__bet : forall A B C D E F, Out B A C -> SuppA A B C D E F -> Bet D E F.
proof: Proof. intros. destruct (segment_construction A B A B) as [B' []]. apply (bet_conga__bet A B B'); trivial. apply (suppa2__conga456 A B C); trivial. assert_diffs. apply suppa_sym, bet_out__suppa; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2