let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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) #); :: thesis: ( 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 ; :: thesis: A "/\" C = C
thus A "/\" C = (SubMeet M) . (A,C) by LATTICES:def 2
.= W /\ ((0). M) by A1, Def8
.= C by Th20 ; :: thesis: verum

end;

hence LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice by Th57, LATTICES:def 13; :: thesis: verum