theorem :: RLSUB_1:72

for V being RealLinearSpace
for v being VECTOR of V holds {v} is Coset of (0). V