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 )