:: deftheorem Def3 defines ZeroCLC CONVEX4:def 3 :
for V being non empty addLoopStr
for b₂ being C_Linear_Combination of V holds
( b₂ = ZeroCLC V iff Carrier b₂ = {} );