proposition: Lemma orthonormal_family_axiom_implies_space_separation : orthonormal_family_axiom -> space_separation_axiom.
proof: Proof. intros up A B C X Y HX HY. destruct (tsp_dec A B C X Y). left; assumption. right; apply (orthonormal_family_axiom_implies_not_two_sides_one_side up); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv