let V be RealLinearSpace; :: 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:34
.= (((1 - a) * u1) - ((1 - a) * v1)) + ((a * u2) - (a * v2)) by RLVECT_1:34
.= ((((1 - a) * u1) + (- ((1 - a) * v1))) + (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)) + ((- ((1 - a) * v1)) + (- (a * v2))) by RLVECT_1:def 3
.= (((1 - a) * u1) + (a * u2)) - (((1 - a) * v1) + (a * v2)) by RLVECT_1:31 ;
( ((1 - a) * u1) + (a * u2) in M & ((1 - a) * v1) + (a * v2) in N ) by A4, A6, RUSUB_4:def 4;
hence ((1 - a) * x) + (a * y) in M - N by A7; :: thesis: verum

end;

hence M - N is Affine by RUSUB_4:def 4; :: thesis: verum