True ↔ ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet A → MeasureTheory.volume A = ⊤ → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, ∃ d ∈ A, EuclideanGeometry.IsIsoscelesTrapezoid a b c d ∧ MeasureTheory.volume ((convexHull ℝ) {a, b, c, d}) = 1