theorem Th59: :: RUSUB_1:59

for V being RealUnitarySpace
for W being Subspace of V
for v1, v2 being VECTOR of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )