let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for M being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let M be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for W1, W2 being Subspace of M holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let W1, W2 be Subspace of M; :: thesis: the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
thus the carrier of (W1 /\ (W1 + W2)) c= the carrier of W1 :: according to XBOOLE_0:def 10 :: thesis: the carrier of W1 c= the carrier of (W1 /\ (W1 + W2))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W1 /\ (W1 + W2)) or x in the carrier of W1 )
assume A1: x in the carrier of (W1 /\ (W1 + W2)) ; :: thesis: x in the carrier of W1
the carrier of (W1 /\ (W1 + W2)) = the carrier of W1 /\ the carrier of (W1 + W2) by Def2;
hence x in the carrier of W1 by A1, XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W1 or x in the carrier of (W1 /\ (W1 + W2)) )
assume A2: x in the carrier of W1 ; :: thesis: x in the carrier of (W1 /\ (W1 + W2))
the carrier of W1 c= the carrier of M by VECTSP_4:def 2;
then reconsider x1 = x as Element of M by A2;
( x1 + (0. M) = x1 & 0. M in W2 & x in W1 ) by A2, RLVECT_1:10, STRUCT_0:def 5, VECTSP_4:25;
then x in { (u + v) where u, v is Element of M : ( u in W1 & v in W2 ) } ;
then x in the carrier of (W1 + W2) by Def1;
then x in the carrier of W1 /\ the carrier of (W1 + W2) by A2, XBOOLE_0:def 4;
hence x in the carrier of (W1 /\ (W1 + W2)) by Def2; :: thesis: verum