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

proof

let x be set ; :: thesis: ( x in M - {v} implies x in union { (M - {u}) where u is VECTOR of V : u in M } )
assume A2: x in M - {v} ; :: thesis: x in union { (M - {u}) where u is VECTOR of V : u in M }
M - {v} in { (M - {u}) where u is VECTOR of V : u in M } by A1;
hence x in union { (M - {u}) where u is VECTOR of V : u in M } by A2, TARSKI:def 4; :: thesis: verum

end;

then A3: M - {v} c= union { (M - {u}) where u is VECTOR of V : u in M } by TARSKI:def 3;
for x being set st x in union { (M - {u}) where u is VECTOR of V : u in M } holds
x in M - {v}

proof

let x be set ; :: thesis: ( x in union { (M - {u}) where u is VECTOR of V : u in M } implies x in M - {v} )
assume x in union { (M - {u}) where u is VECTOR of V : u in M } ; :: thesis: x in M - {v}
then consider N being set such that
A4: ( x in N & N in { (M - {u}) where u is VECTOR of V : u in M } ) by TARSKI:def 4;
consider v1 being VECTOR of V such that
A5: ( N = M - {v1} & v1 in M ) by A4;
thus x in M - {v} by A1, A4, A5, Th17; :: thesis: verum

end;

then union { (M - {u}) where u is VECTOR of V : u in M } c= M - {v} by TARSKI:def 3;
hence M - {v} = union { (M - {u}) where u is VECTOR of V : u in M } by A3, XBOOLE_0:def 10; :: thesis: verum