theorem :: CIRCLED1:19

for V being RealLinearSpace
for v being VECTOR of V ex L being circled_Combination of V st
( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is circled_Combination of A ) )