theorem :: RLSUB_1:73

for V being RealLinearSpace
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being VECTOR of V st V1 = {v}