theorem :: ZMODUL01:128

for V being Z_Module
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W holds W is Linear_Compl of L