theorem :: LOPBAN15:13

for X being RealLinearSpace
for Y being Subspace of X holds RLSp2RVSp Y is Subspace of RLSp2RVSp X ;