set VW2 = the carrier of W2;
set VW1 = the carrier of W1;
set VV = the carrier of V;
0. V in W2 by RLSUB_1:17;
then A1: 0. V in the carrier of W2 by STRUCT_0:def 5;
( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by RLSUB_1: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 the carrier of V by RLSUB_1:def 2;
( V1 is linearly-closed & V2 is linearly-closed ) by RLSUB_1:34;
then A2: V3 is linearly-closed by RLSUB_1:7;
0. V in W1 by RLSUB_1:17;
then 0. V 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 V st the carrier of b₁ = the carrier of W1 /\ the carrier of W2 by A2, RLSUB_1:35; :: thesis: verum