proposition: Lemma par_perp2__par : forall A B C D E F G H, Par A B C D -> Perp A B E F -> Perp C D G H -> Par E F G H.
proof: Proof. intros A B C D; intros. apply (cop4_par_perp2__par A B C D); try (apply all_coplanar); assumption. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID