let R be Ring; :: thesis: for V being RightMod of R
for W being strict Submodule of V holds W /\ W = W
let V be RightMod of R; :: thesis: for W being strict Submodule of V holds W /\ W = W
let W be strict Submodule of V; :: thesis: W /\ W = W
the carrier of W = the carrier of W /\ the carrier of W ;
hence W /\ W = W by Def2; :: thesis: verum