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 A1: ( x in M /\ N & y in M /\ N ) ; :: thesis: ((1 - a) * x) + (a * y) in M /\ N
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: verum

end;

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