theorem :: VECTSP_8:5

for F being Field
for VS being strict VectSp of F holds the L_join of (lattice VS) = SubJoin VS ;