theorem LMQ04: :: NORMSP_3:53

for X being RealLinearSpace
for Y being Subspace of X
for x being object holds
( x is Coset of Y iff x is Coset of RLSp2RVSp Y )