let R be Ring; :: thesis: for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice
let V be RightMod of R; :: thesis: 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
;
:: 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 )
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 Th25
;
:: thesis: A "/\" C = C
thus A "/\" C =
(SubMeet V) . A,
C
by LATTICES:def 2
.=
W /\ ((0). V)
by A1, Def7
.=
C
by Th25
;
:: thesis: verum
end;
hence
LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 0_Lattice
by Th63, LATTICES:def 13; :: thesis: verum