proposition: Lemma os2__inangle : forall A B C P, OS B A C P -> OS B C A P -> InAngle P A B C.
proof: Proof. intros A B C P Hos1 Hos2. apply os_ts__inangle; auto. apply l9_31; Side. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2