:: deftheorem defines NormVSets NORMSP_3:def 17 :
for V being RealNormSpace
for W being Subspace of V
for v being VECTOR of V holds NormVSets (V,W,v) = { ||.x.|| where x is VECTOR of V : x in v + W } ;