let V be Z_Module; :: thesis: LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is lower-bounded
set S = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #);
ex C being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) st
for A being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds
( C "/\" A = C & A "/\" C = C )

proof

reconsider C = (0). V as Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) by Def16;
take C ; :: thesis: for A being Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) holds
( C "/\" A = C & A "/\" C = C )
let A be Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #); :: thesis: ( C "/\" A = C & A "/\" C = C )
reconsider W = A as Submodule of V by Def16;
thus C "/\" A = ((0). V) /\ W by Def22
.= C by Th107 ; :: thesis: A "/\" C = C
hence A "/\" C = C ; :: thesis: verum

end;

hence LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is lower-bounded ; :: thesis: verum