for V being RealLinearSpace
for M being non empty Subset of V holds
( M is convex iff { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M ) by Lm1, Lm3;