proposition: Lemma l12_16_2D : forall A1 A2 B1 B2 C1 C2 X, Par A1 A2 B1 B2 -> Inter A1 A2 C1 C2 X -> exists Y, Inter B1 B2 C1 C2 Y.
proof: Proof. intros. assert (HC := all_coplanar B1 B2 C1 C2). apply l12_16 with A1 A2 X; assumption. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID