for V being Z_Module
for I, I1 being linearly-independent Subset of V st I1 c= I holds
(Lin (I \ I1)) /\ (Lin I1) = (0). V