let V be torsion-free Z_Module; :: thesis: for W1, W2 being free finite-rank Subspace of V st rank (W1 + W2) = rank W2 holds
rank (W1 /\ W2) = rank W1
let W1, W2 be free finite-rank Subspace of V; :: thesis: ( rank (W1 + W2) = rank W2 implies rank (W1 /\ W2) = rank W1 )
assume rank (W1 + W2) = rank W2 ; :: thesis: rank (W1 /\ W2) = rank W1
then (rank W2) + (rank (W1 /\ W2)) = (rank W1) + (rank W2) by LmISRank51X;
hence rank (W1 /\ W2) = rank W1 ; :: thesis: verum