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) )
A1: N + ((- 1) * M) = { (u + w) where u, w is Point of X : ( u in N & w in (- 1) * M ) } by RUSUB_4:def 9;

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

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

end;

assume v in N + (- M) ; :: thesis: v + M meets N
then consider u, w being Point of X such that
A8: v = u + w and
A9: u in N and
A10: w in (- 1) * M by A1;
consider w9 being Point of X such that
A11: w = (- 1) * w9 and
A12: w9 in M by A10;
A13: (- 1) * w = ((- 1) * (- 1)) * w9 by A11, RLVECT_1:def 7
.= w9 by RLVECT_1:def 8 ;
v + w9 = u + (w + w9) by A8, RLVECT_1:def 3
.= u + (w + (- w)) by A13, RLVECT_1:16
.= u + (0. X) by RLVECT_1:5
.= u ;
then u in v + M by A12, Lm1;
hence v + M meets N by A9, XBOOLE_0:3; :: thesis: verum