proposition: Lemma l6_2 : forall A B C P, A<>P -> B<>P -> C<>P -> Bet A P C -> (Bet B P C <-> Out P A B).
proof: Proof. intros. unfold Out. split. intros. repeat split; try assumption; eapply l5_2;eBetween. intro; spliter; induction H5; eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le