theorem :: ZMODUL06:23
for V being Z_Module
for A1, A2 being Subset of V st A1 is linearly-independent & A2 is linearly-independent & A1 /\ A2 = {} & A1 \/ A2 is linearly-dependent holds
(Lin A1) /\ (Lin A2) <> (0). V