let R be Ring; for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice
let V be RightMod of R; LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice
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 Def3;
take
C
;
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) #);
( C "/\" A = C & A "/\" C = C )
consider W being
strict Submodule of
V such that A1:
W = A
by Def3;
thus C "/\" A =
(SubMeet V) . (
C,
A)
by LATTICES:def 2
.=
((0). V) /\ W
by A1, Def7
.=
C
by Th21
;
A "/\" C = C
thus A "/\" C =
(SubMeet V) . (
A,
C)
by LATTICES:def 2
.=
W /\ ((0). V)
by A1, Def7
.=
C
by Th21
;
verum
end;
hence
LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice
by Th47, LATTICES:def 13; verum