TheoremsCoplanar, Cospherical, subset, affineIndependent, affineIndependent_of_mem_of_ne, affineIndependent_of_ne, subset, dist_left_right, dist_left_right_div_two, left_eq_of_isDiameter, left_eq_right_iff, left_mem, left_ne_right_iff_radius_ne_zero, left_ne_right_iff_radius_pos, midpoint_eq_center, ofDiameter_eq, pointReflection_center_left, pointReflection_center_right, right_eq_of_isDiameter, right_mem, sbtw, wbtw, center_eq_iff_eq_of_mem, center_mem_iff, center_ne_iff_ne_of_mem, coe_mk, cospherical, ext, ext_iff, isDiameter_comm, isDiameter_iff_left_mem_and_midpoint_eq_center, isDiameter_iff_left_mem_and_pointReflection_center_left, isDiameter_iff_mem_and_mem_and_dist, isDiameter_iff_mem_and_mem_and_wbtw, isDiameter_iff_ofDiameter_eq, isDiameter_iff_right_mem_and_midpoint_eq_center, isDiameter_iff_right_mem_and_pointReflection_center_right, isDiameter_ofDiameter, mem_coe, mem_coe', mk_center, mk_center_radius, mk_radius, ne_iff, nonempty_iff, radius_nonneg_of_mem, concyclic_empty, concyclic_pair, concyclic_singleton, cospherical_def, cospherical_empty, cospherical_iff_exists_sphere, cospherical_pair, cospherical_singleton, dist_center_eq_dist_center_of_mem_sphere, dist_center_eq_dist_center_of_mem_sphere', dist_of_mem_subset_mk_sphere, dist_of_mem_subset_sphere, eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two, eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two, inner_nonneg_of_dist_le_radius, inner_pos_of_dist_lt_radius, inner_pos_or_eq_of_dist_le_radius, inner_vsub_vsub_of_mem_sphere_of_mem_sphere, instNonemptySphere, mem_sphere, mem_sphere', sbtw_of_collinear_of_dist_center_lt_radius, subset_sphere, wbtw_of_collinear_of_dist_center_le_radius | 70 |