theorem Th46: :: RUSUB_1:46

for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u in W iff v + W = (v + u) + W )