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 object st x in union { (M - {u}) where u is VECTOR of V : u in M } holds
x in M - {v}
proof
let x be object ; :: 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
A2: x in N and
A3: N in { (M - {u}) where u is VECTOR of V : u in M } by TARSKI:def 4;
ex v1 being VECTOR of V st
( N = M - {v1} & v1 in M ) by A3;
hence x in M - {v} by A1, A2, Th17; :: thesis: verum
end;
then A4: union { (M - {u}) where u is VECTOR of V : u in M } c= M - {v} ;
for x being object st x in M - {v} holds
x in union { (M - {u}) where u is VECTOR of V : u in M }
proof
let x be object ; :: thesis: ( x in M - {v} implies x in union { (M - {u}) where u is VECTOR of V : u in M } )
assume A5: 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 A5, TARSKI:def 4; :: thesis: verum
end;
then M - {v} c= union { (M - {u}) where u is VECTOR of V : u in M } ;
hence M - {v} = union { (M - {u}) where u is VECTOR of V : u in M } by A4; :: thesis: verum