let V be torsion-free Z_Module; :: thesis: for W1, W2 being free finite-rank Subspace of V st rank (W1 /\ W2) = rank W1 holds
rank (W1 + W2) = rank W2
let W1, W2 be free finite-rank Subspace of V; :: thesis: ( rank (W1 /\ W2) = rank W1 implies rank (W1 + W2) = rank W2 )
assume A1: rank (W1 /\ W2) = rank W1 ; :: thesis: rank (W1 + W2) = rank W2
set I = the Basis of W1;
for v being Vector of V st v in the Basis of W1 holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V by A1, LmISRank41;
hence rank (W1 + W2) = rank W2 by LmISRank42; :: thesis: verum