:: deftheorem Def4 defines C_Linear_Combination CONVEX4:def 4 :
for V being non empty addLoopStr
for A being Subset of V
for b₃ being C_Linear_Combination of V holds
( b₃ is C_Linear_Combination of A iff Carrier b₃ c= A );