theorem :: VECTSP_8:3

for F being Field
for VS being strict VectSp of F holds Subspaces VS = the carrier of (lattice VS) ;