let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over 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 vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over 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 object ; :: 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 object ; :: 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;
A3: ( x1 + (0. M) = x1 & 0. M in W2 ) by RLVECT_1:4, VECTSP_4:17;
x in W1 by A2, STRUCT_0:def 5;
then x in { (u + v) where v, u is Element of M : ( u in W1 & v in W2 ) } by A3;
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