:: deftheorem Def2 defines Cadditively-linearly-closed CC0SP1:def 2 :
for V being ComplexAlgebra
for V1 being Subset of V holds
( V1 is Cadditively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Complex
for v being Element of V st v in V1 holds
a * v in V1 ) ) );