for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )