:: deftheorem Def5 defines Add_ RSSPACE:def 8 :
for X being RealLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Add_ (X1,X) = the addF of X || X1;