proposition: Theorem upper_dim_3_equivalent_axioms : all_equiv (upper_dim_3_axiom:: orthonormal_family_axiom:: space_separation_axiom:: plane_intersection_axiom:: median_planes_axiom:: nil).
proof: Proof. assert (H := upper_dim_implies_orthonormal_family_axiom). assert (I := orthonormal_family_axiom_implies_space_separation). assert (J := space_separation_implies_plane_intersection). assert (K := plane_intersection_implies_space_separation). assert (L := space_separation_implies_median_planes). assert (M := median_planes_implies_upper_dim). apply all_equiv__equiv; unfold all_equiv'; simpl; repeat split; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv