let V be RealLinearSpace; :: thesis: for M being non empty Subset of V st { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M holds
M is convex
let M be non empty Subset of V; :: thesis: ( { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M implies M is convex )
assume A1: { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M ; :: thesis: M is convex
for u, v being VECTOR of V
for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M

proof

let u, v be VECTOR of V; :: thesis: for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M
let r be Real; :: thesis: ( 0 < r & r < 1 & u in M & v in M implies (r * u) + ((1 - r) * v) in M )
set S = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ;
assume A2: ( 0 < r & r < 1 & u in M & v in M ) ; :: thesis: (r * u) + ((1 - r) * v) in M
consider Lu being Convex_Combination of V such that
A3: ( Sum Lu = u & ( for A being non empty Subset of V st u in A holds
Lu is Convex_Combination of A ) ) by Th1;
reconsider Lu = Lu as Convex_Combination of M by A2, A3;
consider Lv being Convex_Combination of V such that
A4: ( Sum Lv = v & ( for A being non empty Subset of V st v in A holds
Lv is Convex_Combination of A ) ) by Th1;
reconsider Lv = Lv as Convex_Combination of M by A2, A4;
A5: (r * u) + ((1 - r) * v) = (Sum (r * Lu)) + ((1 - r) * (Sum Lv)) by A3, A4, RLVECT_3:2
.= (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:2
.= Sum ((r * Lu) + ((1 - r) * Lv)) by RLVECT_3:1 ;
A6: (r * Lu) + ((1 - r) * Lv) is Convex_Combination of M by A2, CONVEX2:10;
then (r * Lu) + ((1 - r) * Lv) in ConvexComb V by Def1;
then (r * u) + ((1 - r) * v) in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } by A5, A6;
hence (r * u) + ((1 - r) * v) in M by A1; :: thesis: verum

end;

hence M is convex by CONVEX1:def 2; :: thesis: verum