let V be non empty Abelian add-associative RealLinearSpace-like RLSStruct ; :: thesis: for M, N being Subset of V st M is convex & N is convex holds
M + N is convex
let M, N be Subset of V; :: thesis: ( M is convex & N is convex implies M + N is convex )
assume that
A1: M is convex and
A2: N is convex ; :: thesis: M + N is convex
for u, v being VECTOR of V
for r being Real st 0 < r & r < 1 & u in M + N & v in M + N holds
(r * u) + ((1 - r) * v) in M + N

proof

let u, v be VECTOR of V; :: thesis: for r being Real st 0 < r & r < 1 & u in M + N & v in M + N holds
(r * u) + ((1 - r) * v) in M + N
let r be Real; :: thesis: ( 0 < r & r < 1 & u in M + N & v in M + N implies (r * u) + ((1 - r) * v) in M + N )
assume A3: ( 0 < r & r < 1 & u in M + N & v in M + N ) ; :: thesis: (r * u) + ((1 - r) * v) in M + N
then u in { (x + y) where x, y is Element of V : ( x in M & y in N ) } by RUSUB_4:def 10;
then consider x1, y1 being Element of V such that
A4: ( u = x1 + y1 & x1 in M & y1 in N ) ;
v in { (x + y) where x, y is Element of V : ( x in M & y in N ) } by A3, RUSUB_4:def 10;
then consider x2, y2 being Element of V such that
A5: ( v = x2 + y2 & x2 in M & y2 in N ) ;
A6: (r * x1) + ((1 - r) * x2) in M by A1, A3, A4, A5, Def2;
A7: (r * y1) + ((1 - r) * y2) in N by A2, A3, A4, A5, Def2;
(r * u) + ((1 - r) * v) = ((r * x1) + (r * y1)) + ((1 - r) * (x2 + y2)) by A4, A5, RLVECT_1:def 9
.= ((r * x1) + (r * y1)) + (((1 - r) * x2) + ((1 - r) * y2)) by RLVECT_1:def 9
.= (((r * x1) + (r * y1)) + ((1 - r) * x2)) + ((1 - r) * y2) by RLVECT_1:def 6
.= (((r * x1) + ((1 - r) * x2)) + (r * y1)) + ((1 - r) * y2) by RLVECT_1:def 6
.= ((r * x1) + ((1 - r) * x2)) + ((r * y1) + ((1 - r) * y2)) by RLVECT_1:def 6 ;
then (r * u) + ((1 - r) * v) in { (x + y) where x, y is Element of V : ( x in M & y in N ) } by A6, A7;
hence (r * u) + ((1 - r) * v) in M + N by RUSUB_4:def 10; :: thesis: verum

end;

hence M + N is convex by Def2; :: thesis: verum