∀ (A B C P L M N : EuclideanSpace ℝ (Fin 2)), AffineIndependent ℝ ![A, B, C] → P ∈ interior ((convexHull ℝ) {A, B, C}) → N ∈ affineSpan ℝ {A, B} → (affineSpan ℝ {P, N}).direction ⟂ (affineSpan ℝ {A, B}).direction → M ∈ affineSpan ℝ {B, C} → (affineSpan ℝ {P, M}).direction ⟂ (affineSpan ℝ {B, C}).direction → L ∈ affineSpan ℝ {C, A} → (affineSpan ℝ {P, L}).direction ⟂ (affineSpan ℝ {C, A}).direction → dist P A + dist P B + dist P C ≥ 2 * (dist P M + dist P N + dist P L)