∀ {V : Type u_2} {P : Type u_10} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] [inst_3 : NormedSpace ℝ V] (x y : P),
  (AffineIsometryEquiv.pointReflection ℝ (midpoint ℝ x y)) y = x