theorem :: ZMODUL01:126

for V being Z_Module
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W holds W /\ L = (0). V