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_{1} being strict Subspace of V st the carrier of b_{1} = the carrier of W1 /\ the carrier of W2
by A2, RLSUB_1:35; :: thesis: verum

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