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

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

hence
M /\ N is Affine
; :: thesis: verum
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;((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