theorem LMQ07: :: NORMSP_3:56

for V being RealLinearSpace
for W being Subspace of V
for x being object holds
( x is Point of (VectQuot (V,W)) iff ex v being Point of V st x = v + W )