let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for M being Affine Subset of V

for v being VECTOR of V holds {v} + M is Affine

let M be Affine Subset of V; :: thesis: for v being VECTOR of V holds {v} + M is Affine

let v be VECTOR of V; :: thesis: {v} + M is Affine

{v} + M = v + M by Th33;

hence {v} + M is Affine by Th31; :: thesis: verum

for v being VECTOR of V holds {v} + M is Affine

let M be Affine Subset of V; :: thesis: for v being VECTOR of V holds {v} + M is Affine

let v be VECTOR of V; :: thesis: {v} + M is Affine

{v} + M = v + M by Th33;

hence {v} + M is Affine by Th31; :: thesis: verum