proposition: Lemma between_inner_transitivity_B : forall A B C D : Tpoint, BetH A B D -> BetH B C D -> BetH A B C.
proof: Proof. intros A B C D HBet1 HBet2. unfold BetH. repeat split. apply BetH_Bet in HBet1. apply BetH_Bet in HBet2. apply between_inner_transitivity with D; assumption. unfold BetH in HBet1. spliter; assumption. unfold BetH in HBet2. spliter; assumption. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality