theorem :: VECTSP_8:4

for F being Field
for VS being strict VectSp of F holds the L_meet of (lattice VS) = SubMeet VS ;