theorem :: VECTSP_5:62

for F being Field
for V being VectSp of F holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice