:: deftheorem defines additively-linearly-closed C0SP1:def 10 :
for V being Algebra
for V1 being Subset of V holds
( V1 is additively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Real
for v being Element of V st v in V1 holds
a * v in V1 ) ) );