for V being RealLinearSpace
for W being strict Subspace of V holds W is strict Subspace of (Omega). V