let V be Z_Module; :: thesis: for W being strict Submodule of V holds ((Omega). V) /\ W = W
let W be strict Submodule of V; :: thesis: ((Omega). V) /\ W = W
( the carrier of (((Omega). V) /\ W) = the carrier of V /\ the carrier of W & the carrier of W c= the carrier of V ) by Def15, Def9;
hence ((Omega). V) /\ W = W by Th45, XBOOLE_1:28; :: thesis: verum