theorem :: RLSUB_1:81

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