Convex independence passes to finite subsets

import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_Foundation
import Mathlib.Analysis.Convex.Between
import Mathlib.Analysis.Convex.Independent
import Mathlib.Data.Finset.Basic
import Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
open Problem97 Problem97.ConvexIndep
open scoped EuclideanGeometry

theorem Batch3N9.Problem97.ConvexIndep.mono {A B : Finset ℝ²} (hBA : B ⊆ A) (hA : ConvexIndep A) : ConvexIndep B := by sorry