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 A1: ( M is Subspace-like & v in M ) ; :: thesis: M + {v} c= M
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in M + {v} or x in M )
assume A2: 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 A2, RUSUB_4:def 9;
then consider u1, v1 being Element of V such that
A3: ( x = u1 + v1 & u1 in M ) and
A4: v1 in {v} ;
v1 = v by A4, TARSKI:def 1;
hence x in M by A1, A3, RUSUB_4:def 7; :: thesis: verum