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 being Subspace of M
for W2 being strict Subspace of M st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let M be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for W1 being Subspace of M
for W2 being strict Subspace of M st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let W1 be Subspace of M; :: thesis: for W2 being strict Subspace of M st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let W2 be strict Subspace of M; :: thesis: ( the carrier of W1 c= the carrier of W2 implies W1 + W2 = W2 )
assume A1: the carrier of W1 c= the carrier of W2 ; :: thesis: W1 + W2 = W2
the carrier of (W1 + W2) = the carrier of W2

proof

thus the carrier of (W1 + W2) c= the carrier of W2 :: according to XBOOLE_0:def 10 :: thesis: the carrier of W2 c= the carrier of (W1 + W2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W1 + W2) or x in the carrier of W2 )
assume x in the carrier of (W1 + W2) ; :: thesis: x in the carrier of W2
then x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } by Def1;
then consider v, u being Element of M such that
A2: x = v + u and
A3: v in W1 and
A4: u in W2 ;
W1 is Subspace of W2 by A1, VECTSP_4:35;
then v in W2 by A3, VECTSP_4:16;
then v + u in W2 by A4, VECTSP_4:28;
hence x in the carrier of W2 by A2, STRUCT_0:def 5; :: thesis: verum

end;

W1 + W2 = W2 + W1 by Lm1;
hence the carrier of W2 c= the carrier of (W1 + W2) by Lm2; :: thesis: verum

end;

hence W1 + W2 = W2 by VECTSP_4:37; :: thesis: verum