let V be torsion-free Z_Module; :: thesis: for W1, W2 being free finite-rank Subspace of V holds rank (W1 /\ W2) <= rank W1
let W1, W2 be free finite-rank Subspace of V; :: thesis: rank (W1 /\ W2) <= rank W1
W1 /\ W2 is Subspace of W1 by ZMODUL01:105;
hence rank (W1 /\ W2) <= rank W1 by ZMODUL05:2; :: thesis: verum