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 W being Subspace of M ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
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 W being Subspace of M ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
let W be Subspace of M; :: thesis: ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
take W9 = W + W; :: thesis: the carrier of W = the carrier of W9
thus the carrier of W c= the carrier of W9 by Lm2; :: according to XBOOLE_0:def 10 :: thesis: the carrier of W9 c= the carrier of W
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W9 or x in the carrier of W )
assume x in the carrier of W9 ; :: thesis: x in the carrier of W
then x in { (v + u) where u, v is Element of M : ( v in W & u in W ) } by Def1;
then ex v2, v1 being Element of M st
( x = v1 + v2 & v1 in W & v2 in W ) ;
then x in W by VECTSP_4:20;
hence x in the carrier of W by STRUCT_0:def 5; :: thesis: verum