for V being RealLinearSpace
for M being non empty Subset of V holds conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V }