:: deftheorem Def6 defines Add_ CSSPACE:def 8 :
for X being ComplexLinearSpace
for X1 being Subset of X st X1 is linearly-closed holds
Add_ (X1,X) = the addF of X || X1;