proposition: Lemma prop_28_1 : forall B D E G H, Out E G H -> OS E G B D -> CongA B G E D H E -> Par G B H D.
proof: Proof. intros B D E G H. apply l12_22_b. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions