for F being Field
for V being VectSp of F
for W being Subspace of (Omega). V holds W is Subspace of V