let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for W being Subspace of V holds
( v + W = (- v) + W iff v in W )
let v be VECTOR of V; :: thesis: for W being Subspace of V holds
( v + W = (- v) + W iff v in W )
let W be Subspace of V; :: thesis: ( v + W = (- v) + W iff v in W )
thus ( v + W = (- v) + W implies v in W ) :: thesis: ( v in W implies v + W = (- v) + W )

proof

assume v + W = (- v) + W ; :: thesis: v in W
then v in (- v) + W by Th43;
then consider u being VECTOR of V such that
A1: v = (- v) + u and
A2: u in W ;
reconsider dwa = 2 as Real ;
0. V = v - ((- v) + u) by A1, RLVECT_1:15
.= (v - (- v)) - u by RLVECT_1:27
.= (v + v) - u
.= ((1 * v) + v) - u by RLVECT_1:def 8
.= ((1 * v) + (1 * v)) - u by RLVECT_1:def 8
.= ((1 + 1) * v) - u by RLVECT_1:def 6
.= (2 * v) - u ;
then (2 ") * (2 * v) = (2 ") * u by RLVECT_1:21;
then ((2 ") * 2) * v = (2 ") * u by RLVECT_1:def 7;
then v = (dwa ") * u by RLVECT_1:def 8;
hence v in W by A2, Th21; :: thesis: verum

end;

assume A3: v in W ; :: thesis: v + W = (- v) + W
then v + W = the carrier of W by Lm3;
hence v + W = (- v) + W by A3, Th51; :: thesis: verum