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