set VW2 = the carrier of W2;
set VW1 = the carrier of W1;
set VV = the carrier of V;
0. V in W2 by RMOD_2:17;
then A1: 0. V in the carrier of W2 ;
( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by RMOD_2:def 2;
then the carrier of W1 /\ the carrier of W2 c= the carrier of V /\ the carrier of V by XBOOLE_1:27;
then reconsider V1 = the carrier of W1, V2 = the carrier of W2, V3 = the carrier of W1 /\ the carrier of W2 as Subset of V by RMOD_2:def 2;
( V1 is linearly-closed & V2 is linearly-closed ) by RMOD_2:33;
then A2: V3 is linearly-closed by RMOD_2:7;
0. V in W1 by RMOD_2:17;
then 0. V in the carrier of W1 ;
then the carrier of W1 /\ the carrier of W2 <> {} by A1, XBOOLE_0:def 4;
hence ex b₁ being strict Submodule of V st the carrier of b₁ = the carrier of W1 /\ the carrier of W2 by A2, RMOD_2:34; :: thesis: verum