let V be RealLinearSpace; :: thesis: for M being non empty Affine Subset of V
for v being VECTOR of V st M is Subspace-like & v in M holds
M + {v} c= M
let M be non empty Affine Subset of V; :: thesis: for v being VECTOR of V st M is Subspace-like & v in M holds
M + {v} c= M
let v be VECTOR of V; :: thesis: ( M is Subspace-like & v in M implies M + {v} c= M )
assume that
A1: M is Subspace-like and
A2: v in M ; :: thesis: M + {v} c= M
for x being set st x in M + {v} holds
x in M

proof

let x be set ; :: thesis: ( x in M + {v} implies x in M )
assume A3: x in M + {v} ; :: thesis: x in M
then reconsider x = x as Element of V ;
x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in M & v1 in {v} ) } by A3, RUSUB_4:def 10;
then consider u1, v1 being Element of V such that
A4: ( x = u1 + v1 & u1 in M & v1 in {v} ) ;
v1 = v by A4, TARSKI:def 1;
hence x in M by A1, A2, A4, RUSUB_4:def 8; :: thesis: verum

end;

hence M + {v} c= M by TARSKI:def 3; :: thesis: verum