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 Th59;
then consider u being VECTOR of V such that
A1: v = (- v) + u and
A2: u in W ;
0. V = v - ((- v) + u) by A1, RLVECT_1:28
.= (v - (- v)) - u by RLVECT_1:41
.= (v + v) - u by RLVECT_1:30
.= ((1 * v) + v) - u by RLVECT_1:def 9
.= ((1 * v) + (1 * v)) - u by RLVECT_1:def 9
.= ((1 + 1) * v) - u by RLVECT_1:def 9
.= (2 * v) - u ;
then (2 " ) * (2 * v) = (2 " ) * u by RLVECT_1:35;
then ( ((2 " ) * 2) * v = (2 " ) * u & 0 <> 2 ) by RLVECT_1:def 9;
then v = (2 " ) * u by RLVECT_1:def 9;
hence v in W by A2, Th29; :: thesis: verum

end;

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