let R be Ring; :: thesis: for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice
let V be RightMod of R; :: 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 Th48, Th49;
hence LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 01_Lattice ; :: thesis: verum