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} )
assume A1: v in M ; :: thesis: 0. V in M - {v}
A2: v in {v} by TARSKI:def 1;
0. V = v - v by RLVECT_1:28;
hence 0. V in M - {v} by A1, A2; :: thesis: verum