let V be Z_Module; :: thesis: LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice
LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is lower-bounded upper-bounded Lattice by Th144, Th145;
hence LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice ; :: thesis: verum