theorem :: ZMODUL01:41

for V, X being strict Z_Module st V is Submodule of X & X is Submodule of V holds
V = X by VECTSP_4:25;