:: deftheorem defines lattice VECTSP_8:def 1 :
for F being Field
for VS being strict VectSp of F holds lattice VS = LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #);