theorem Th1: :: VECTSP_8:1

for F being Field
for VS being strict VectSp of F
for H being non empty Subset of (Subspaces VS) holds not (carr VS) .: H is empty