W1 /\ W2 is Submodule of W1 by ZMODUL01:105;
hence W1 /\ W2 is finite-rank by RL5Th28; :: thesis: verum