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
0. V in M - {v}
let M be non empty Affine Subset of V; :: thesis: for v being VECTOR of V st v in M holds
0. V in M - {v}
let v be VECTOR of V; :: thesis: ( v in M implies 0. V in M - {v} )
A1: ( v in {v} & 0. V = v - v ) by RLVECT_1:15, TARSKI:def 1;
assume v in M ; :: thesis: 0. V in M - {v}
hence 0. V in M - {v} by A1; :: thesis: verum