let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
ex C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st
for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "/\" A = C & A "/\" C = C )
proof
reconsider C =
(0). M as
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #)
by Def3;
take
C
;
for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "/\" A = C & A "/\" C = C )
let A be
Element of
LattStr(#
(Subspaces M),
(SubJoin M),
(SubMeet M) #);
( C "/\" A = C & A "/\" C = C )
consider W being
strict Subspace of
M such that A1:
W = A
by Def3;
thus C "/\" A =
(SubMeet M) . (
C,
A)
by LATTICES:def 2
.=
((0). M) /\ W
by A1, Def8
.=
C
by Th20
;
A "/\" C = C
thus A "/\" C =
(SubMeet M) . (
A,
C)
by LATTICES:def 2
.=
W /\ ((0). M)
by A1, Def8
.=
C
by Th20
;
verum
end;
hence
LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice
by Th57, LATTICES:def 13; verum