let V be RealLinearSpace; :: thesis:
let M be non empty Affine Subset of V; :: thesis:
let v be VECTOR of V; :: thesis:
( not {v} is empty & {v} is Affine ) by RUSUB_4:23;
then reconsider N = M - {v} as non empty Affine Subset of V by Th4, Th8;
assume v in M ; :: thesis:
then A1: 0. V in N by Th15;
take N ; :: thesis:
M is_parallel_to N

take v ; :: according to RUSUB_5:def 1 :: thesis:
thus M = N + {v} by Th9; :: thesis:

end;