set VW2 = the carrier of W2;
set VW1 = the carrier of W1;
set VV = the carrier of M;
0. M in W2 by VECTSP_4:17;
then A1: 0. M in the carrier of W2 by STRUCT_0:def 5;
( the carrier of W1 c= the carrier of M & the carrier of W2 c= the carrier of M ) by VECTSP_4:def 2;
then the carrier of W1 /\ the carrier of W2 c= the carrier of M /\ the carrier of M 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 M by VECTSP_4:def 2;
( V1 is linearly-closed & V2 is linearly-closed ) by VECTSP_4:33;
then A2: V3 is linearly-closed by VECTSP_4:7;
0. M in W1 by VECTSP_4:17;
then 0. M in the carrier of W1 by STRUCT_0:def 5;
then the carrier of W1 /\ the carrier of W2 <> {} by A1, XBOOLE_0:def 4;
hence ex b₁ being strict Subspace of M st the carrier of b₁ = the carrier of W1 /\ the carrier of W2 by A2, VECTSP_4:34; :: thesis: verum