proposition: Lemma out_bet__out : forall A B P Q, Bet P Q A -> Out Q A B -> Out P A B.
proof: Proof. intros A B P Q HBet Hout. destruct Hout as [HAQ [HBQ [HQAB|HQBA]]]; [|apply l6_6]; apply bet_out; eBetween; intro; treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le