proposition: Lemma l11_15 : forall A B C D E P, ~ Col A B C -> ~ Col D E P -> exists F, CongA A B C D E F /\ OS E D F P /\ (forall F1 F2, ((CongA A B C D E F1 /\ OS E D F1 P) /\ (CongA A B C D E F2 /\ OS E D F2 P)) -> Out E F1 F2).
proof: Proof. intros. assert(exists F, CongA A B C D E F /\ OS D E F P) by (apply angle_construction_1; assumption). ex_and H1 F. exists F. split. assumption. split. apply invert_one_side. assumption. intros. spliter. apply (conga_os__out D). apply conga_trans with A B C. apply conga_sym. assumption. assumption. apply invert_one_side. apply one_side_transitivity with P; Side. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2