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

set S = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ;
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 )
assume that
A2: ( 0 < r & r < 1 ) and
A3: u in M and
A4: v in M ; :: thesis: (r * u) + ((1 - r) * v) in M
consider Lv being Convex_Combination of V such that
A5: Sum Lv = v and
A6: 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 A4, A6;
consider Lu being Convex_Combination of V such that
A7: Sum Lu = u and
A8: 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 A3, A8;
A9: (r * u) + ((1 - r) * v) = (Sum (r * Lu)) + ((1 - r) * (Sum Lv)) by A7, A5, RLVECT_3:2
.= (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:2
.= Sum ((r * Lu) + ((1 - r) * Lv)) by RLVECT_3:1 ;
reconsider r = r as Real ;
A10: (r * Lu) + ((1 - r) * Lv) is Convex_Combination of M by A2, CONVEX2:9;
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 A9, A10;
hence (r * u) + ((1 - r) * v) in M by A1; :: thesis: verum

end;

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