:: deftheorem Def1 defines ConvexComb CONVEX3:def 1 :
for V being RealLinearSpace
for b₂ being set holds
( b₂ = ConvexComb V iff for L being object holds
( L in b₂ iff L is Convex_Combination of V ) );