let V be RealLinearSpace; :: thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded upper-bounded Lattice by Th71, Th72;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice ; :: thesis: verum