let V be Z_Module; :: 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 Def15; :: thesis: verum