proposition: Lemma lemma_3_5b : forall A B C D, BetS A B D -> BetS B C D -> BetS A C D.
proof: Proof. intros. assert (BetS A B C) by (conclude axiom_innertransitivity). assert (BetS A C D) by (conclude lemma_3_7a). close. Qed.
imports: GeoCoq.Elements.OriginalProofs.lemma_3_7a