:: deftheorem defines ConvexComb CONVEX3:def 2 :
for V being RealLinearSpace
for M being non empty Subset of V
for b₃ being set holds
( b₃ = ConvexComb M iff for L being object holds
( L in b₃ iff L is Convex_Combination of M ) );