let X be RealLinearSpace; :: thesis: for M, N being Subset of X
for v being Point of X holds
( v + M meets N iff v in N + (- M) )
let M, N be Subset of X; :: thesis: for v being Point of X holds
( v + M meets N iff v in N + (- M) )
let v be Point of X; :: thesis: ( v + M meets N iff v in N + (- M) )

hereby :: thesis: ( v in N + (- M) implies v + M meets N )

assume v + M meets N ; :: thesis: v in N + (- M)
then consider z being set such that
A1: z in v + M and
A2: z in N by XBOOLE_0:3;
v + M = { (v + u) where u is Point of X : u in M } by RUSUB_4:def 9;
then consider u being Point of X such that
A3: v + u = z and
A4: u in M by A1;
reconsider z = z as Point of X by A1;
A5: z + ((- 1) * u) = v + (u + ((- 1) * u)) by A3, RLVECT_1:def 6
.= v + (u + (- u)) by RLVECT_1:29
.= v + (0. X) by RLVECT_1:16
.= v by RLVECT_1:10 ;
(- 1) * u in (- 1) * M by A4;
hence v in N + (- M) by A2, A5, Th3; :: thesis: verum

end;

A6: N + ((- 1) * M) = { (u + w) where u, w is Point of X : ( u in N & w in (- 1) * M ) } by RUSUB_4:def 10;
assume v in N + (- M) ; :: thesis: v + M meets N
then consider u, w being Point of X such that
A7: v = u + w and
A8: u in N and
A9: w in (- 1) * M by A6;
consider w' being Point of X such that
A10: w = (- 1) * w' and
A11: w' in M by A9;
A12: (- 1) * w = ((- 1) * (- 1)) * w' by A10, RLVECT_1:def 9
.= w' by RLVECT_1:def 9 ;
v + w' = u + (w + w') by A7, RLVECT_1:def 6
.= u + (w + (- w)) by A12, RLVECT_1:29
.= u + (0. X) by RLVECT_1:16
.= u by RLVECT_1:10 ;
then u in v + M by A11, Lm1;
hence v + M meets N by A8, XBOOLE_0:3; :: thesis: verum