let V be RealLinearSpace; :: thesis: for M being non empty Affine Subset of V holds M - M = union { (M - {v}) where v is VECTOR of V : v in M }
let M be non empty Affine Subset of V; :: thesis: M - M = union { (M - {v}) where v is VECTOR of V : v in M }
for x being object st x in M - M holds
x in union { (M - {v}) where v is VECTOR of V : v in M }

proof

let x be object ; :: thesis: ( x in M - M implies x in union { (M - {v}) where v is VECTOR of V : v in M } )
assume A1: x in M - M ; :: thesis: x in union { (M - {v}) where v is VECTOR of V : v in M }
then reconsider x = x as Element of V ;
consider u1, v1 being Element of V such that
A2: ( x = u1 - v1 & u1 in M ) and
A3: v1 in M by A1;
v1 in {v1} by TARSKI:def 1;
then A4: x in { (p - q) where p, q is Element of V : ( p in M & q in {v1} ) } by A2;
M - {v1} in { (M - {v}) where v is VECTOR of V : v in M } by A3;
hence x in union { (M - {v}) where v is VECTOR of V : v in M } by A4, TARSKI:def 4; :: thesis: verum

end;

then A5: M - M c= union { (M - {v}) where v is VECTOR of V : v in M } ;
for x being object st x in union { (M - {v}) where v is VECTOR of V : v in M } holds
x in M - M

proof

let x be object ; :: thesis: ( x in union { (M - {v}) where v is VECTOR of V : v in M } implies x in M - M )
assume x in union { (M - {v}) where v is VECTOR of V : v in M } ; :: thesis: x in M - M
then consider N being set such that
A6: x in N and
A7: N in { (M - {v}) where v is VECTOR of V : v in M } by TARSKI:def 4;
consider v1 being VECTOR of V such that
A8: N = M - {v1} and
A9: v1 in M by A7;
consider p1, q1 being Element of V such that
A10: ( x = p1 - q1 & p1 in M ) and
A11: q1 in {v1} by A6, A8;
q1 = v1 by A11, TARSKI:def 1;
hence x in M - M by A9, A10; :: thesis: verum

end;

then union { (M - {v}) where v is VECTOR of V : v in M } c= M - M ;
hence M - M = union { (M - {v}) where v is VECTOR of V : v in M } by A5; :: thesis: verum