for V being RealLinearSpace
for A being Subset of V holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )