theorem Th65: :: RLSUB_1:65

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