let V be free finite-rank Z_Module; :: thesis: for W1, W2 being Submodule of V holds rank (W1 /\ W2) >= ((rank W1) + (rank W2)) - (rank V)
let W1, W2 be Submodule of V; :: thesis: rank (W1 /\ W2) >= ((rank W1) + (rank W2)) - (rank V)
A1: ( rank (W1 + W2) <= rank V & (rank V) + ((rank (W1 /\ W2)) - (rank V)) = rank (W1 /\ W2) ) by ZMODUL05:2;
((rank W1) + (rank W2)) - (rank V) = ((rank (W1 + W2)) + (rank (W1 /\ W2))) - (rank V) by ZMODUL06:62
.= (rank (W1 + W2)) + ((rank (W1 /\ W2)) - (rank V)) ;
hence rank (W1 /\ W2) >= ((rank W1) + (rank W2)) - (rank V) by A1, XREAL_1:6; :: thesis: verum