proposition: Lemma l9_19_3 : forall A B C X Y P, Coplanar A B C P -> Col X Y P -> OSP A B C X Y <-> Out P X Y /\ ~ Coplanar A B C X.
proof: Proof. intros A B C X Y P HP HCol. split; [|intros []; apply cop_out__osp with P; assumption]. intro HOS. assert (~ Coplanar A B C X /\ ~ Coplanar A B C Y). unfold OSP, TSP in HOS; destruct HOS as [Z []]; spliter; split; assumption. spliter. split; [|assumption]. apply not_bet_out; [Col|]. intro HBet. apply osp__ntsp in HOS. apply HOS. repeat split; trivial; exists P; split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar