∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x₁ x₂ y z : V},
  x₁ ≠ y →
    x₁ ≠ z →
      x₂ ≠ y →
        x₂ ≠ z →
          ∀ {r : ℝ},
            ‖x₁‖ = r → ‖x₂‖ = r → ‖y‖ = r → ‖z‖ = r → 2 • o.oangle (y - x₁) (z - x₁) = 2 • o.oangle (y - x₂) (z - x₂)