let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for M, N being Affine Subset of V holds M + N is Affine
let M, N be Affine Subset of V; :: thesis: M + N is Affine
for x, y being VECTOR of V
for a being Real st x in M + N & y in M + N holds
((1 - a) * x) + (a * y) in M + N

proof

let x, y be VECTOR of V; :: thesis: for a being Real st x in M + N & y in M + N holds
((1 - a) * x) + (a * y) in M + N
let a be Real; :: thesis: ( x in M + N & y in M + N implies ((1 - a) * x) + (a * y) in M + N )
assume that
A1: x in M + N and
A2: y in M + N ; :: thesis: ((1 - a) * x) + (a * y) in M + N
consider u1, v1 being Element of V such that
A3: x = u1 + v1 and
A4: ( u1 in M & v1 in N ) by A1;
consider u2, v2 being Element of V such that
A5: y = u2 + v2 and
A6: ( u2 in M & v2 in N ) by A2;
A7: ((1 - a) * x) + (a * y) = (((1 - a) * u1) + ((1 - a) * v1)) + (a * (u2 + v2)) by A3, A5, RLVECT_1:def 5
.= (((1 - a) * u1) + ((1 - a) * v1)) + ((a * u2) + (a * v2)) by RLVECT_1:def 5
.= ((((1 - a) * u1) + ((1 - a) * v1)) + (a * u2)) + (a * v2) by RLVECT_1:def 3
.= (((1 - a) * v1) + (((1 - a) * u1) + (a * u2))) + (a * v2) by RLVECT_1:def 3
.= (((1 - a) * u1) + (a * u2)) + (((1 - a) * v1) + (a * v2)) by RLVECT_1:def 3 ;
( ((1 - a) * u1) + (a * u2) in M & ((1 - a) * v1) + (a * v2) in N ) by A4, A6, Def4;
hence ((1 - a) * x) + (a * y) in M + N by A7; :: thesis: verum

end;

hence M + N is Affine ; :: thesis: verum