theorem ThStrict1: :: ZMODUL07:37

for V being Z_Module
for W being Submodule of V
for Ws being strict Submodule of V st Ws = (Omega). W holds
Z_ModuleQuot (V,W) = Z_ModuleQuot (V,Ws)