let V be non empty RLSStruct ; :: thesis:
let M, N be Affine Subset of V; :: thesis:
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

let x, y be VECTOR of V; :: thesis:
let a be Real; :: thesis:
assume A1: ( x in M /\ N & y in M /\ N ) ; :: thesis:
then ( x in N & y in N ) by XBOOLE_0:def 4;
then A2: ((1 - a) * x) + (a * y) in N by Def4;
( x in M & y in M ) by A1, XBOOLE_0:def 4;
then ((1 - a) * x) + (a * y) in M by Def4;
hence ((1 - a) * x) + (a * y) in M /\ N by A2, XBOOLE_0:def 4; :: thesis:

end;