proposition: Lemma out2_bet_out : forall A B C X P, Out B A C -> Out B X P -> Bet A X C -> Out B A P /\ Out B C P.
proof: Proof. intros. unfold Out in *. spliter. induction H5; induction H3. repeat split; try assumption. left; eapply between_exchange4 with X; try assumption. apply between_inner_transitivity with C; assumption. apply l5_1 with X; try auto. apply between_exchange2 with A; assumption. repeat split; try assumption. apply l5_3 with X; try assumption. apply between_inner_transitivity with C; assumption. right; apply between_exchange4 with X; try assumption. apply between_exchange2 with A; assumption. repeat split; try assumption. apply l5_1 with X; try auto. apply between_exchange2 with C; Between. left; apply between_exchange4 with X; try assumption. apply between_inner_transitivity with A; Between. repeat split; try assumption. right; apply between_exchange4 with X; try assumption. apply between_exchange2 with C; Between. apply l5_3 with X; try assumption. apply between_inner_transitivity with A; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le