:: deftheorem defines + RLSUB_1:def 5 :
for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds v + W = { (v + u) where u is VECTOR of V : u in W } ;