proposition: Lemma l9_18_3 : forall A B C X Y P, Coplanar A B C P -> Col X Y P -> TSP A B C X Y <-> Bet X P Y /\ ~ Coplanar A B C X /\ ~ Coplanar A B C Y.
proof: Proof. intros A B C X Y P HP HCol. split; [|intros [HBet [HX HY]]; repeat split; trivial; exists P; split; assumption]. intros [HX [HY [T [HT HBet]]]]. repeat split; trivial. replace P with T; trivial. apply (col2_cop2__eq A B C X Y); Col. intro; treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar