let V be RealLinearSpace; :: thesis: for v1, v2 being VECTOR of V
for W being Subspace of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
let v1, v2 be VECTOR of V; :: thesis: for W being Subspace of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
let W be Subspace of V; :: thesis: ( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
thus ( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) implies v1 - v2 in W ) :: thesis: ( v1 - v2 in W implies ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) )

proof

given v being VECTOR of V such that A1: v1 in v + W and
A2: v2 in v + W ; :: thesis: v1 - v2 in W
consider u2 being VECTOR of V such that
A3: u2 in W and
A4: v2 = v + u2 by A2, Th63;
consider u1 being VECTOR of V such that
A5: u1 in W and
A6: v1 = v + u1 by A1, Th63;
v1 - v2 = (u1 + v) + ((- v) - u2) by A6, A4, RLVECT_1:30
.= ((u1 + v) + (- v)) - u2 by RLVECT_1:def 3
.= (u1 + (v + (- v))) - u2 by RLVECT_1:def 3
.= (u1 + (0. V)) - u2 by RLVECT_1:5
.= u1 - u2 ;
hence v1 - v2 in W by A5, A3, Th23; :: thesis: verum

end;

assume v1 - v2 in W ; :: thesis: ex v being VECTOR of V st
( v1 in v + W & v2 in v + W )
then A7: - (v1 - v2) in W by Th22;
take v1 ; :: thesis: ( v1 in v1 + W & v2 in v1 + W )
thus v1 in v1 + W by Th43; :: thesis: v2 in v1 + W
v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by RLVECT_1:33
.= (v1 + (- v1)) + v2 by RLVECT_1:def 3
.= (0. V) + v2 by RLVECT_1:5
.= v2 ;
hence v2 in v1 + W by A7; :: thesis: verum