let V be RealLinearSpace; :: thesis: for M being non empty Affine Subset of V
for u, v being VECTOR of V st u in M & v in M holds
M - {v} = M - {u}
let M be non empty Affine Subset of V; :: thesis: for u, v being VECTOR of V st u in M & v in M holds
M - {v} = M - {u}
let u, v be VECTOR of V; :: thesis: ( u in M & v in M implies M - {v} = M - {u} )
assume ( u in M & v in M ) ; :: thesis: M - {v} = M - {u}
then ( ex N1 being non empty Affine Subset of V st
( N1 = M - {u} & M is_parallel_to N1 & N1 is Subspace-like ) & ex N2 being non empty Affine Subset of V st
( N2 = M - {v} & M is_parallel_to N2 & N2 is Subspace-like ) ) by Th16;
hence M - {v} = M - {u} by Th14; :: thesis: verum