let V be non empty 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 ( x in M /\ N & y in M /\ N ) ; :: thesis: ((1 - a) * x) + (a * y) in M /\ N
then ( x in M & x in N & y in M & y in N ) by XBOOLE_0:def 4;
then ( ((1 - a) * x) + (a * y) in M & ((1 - a) * x) + (a * y) in N ) by Def5;
hence ((1 - a) * x) + (a * y) in M /\ N by XBOOLE_0:def 4; :: thesis: verum

end;

hence M /\ N is Affine by Def5; :: thesis: verum