let V be non empty Abelian CLSStruct ; :: thesis: for M being Subset of V st M is convex holds
for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
((1r - z) * M) + (z * M) c= M
let M be Subset of V; :: thesis: ( M is convex implies for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
((1r - z) * M) + (z * M) c= M )
assume A1: M is convex ; :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
((1r - z) * M) + (z * M) c= M
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) implies ((1r - z) * M) + (z * M) c= M )
assume A2: ex r being Real st
( z = r & 0 < r & r < 1 ) ; :: thesis: ((1r - z) * M) + (z * M) c= M
for x being Element of V st x in ((1r - z) * M) + (z * M) holds
x in M
proof
let x be Element of V; :: thesis: ( x in ((1r - z) * M) + (z * M) implies x in M )
assume x in ((1r - z) * M) + (z * M) ; :: thesis: x in M
then consider u, v being Element of V such that
A3: x = u + v and
A4: ( u in (1r - z) * M & v in z * M ) ;
( ex w1 being Element of V st
( u = (1r - z) * w1 & w1 in M ) & ex w2 being Element of V st
( v = z * w2 & w2 in M ) ) by A4;
hence x in M by A1, A2, A3; :: thesis: verum
end;
hence ((1r - z) * M) + (z * M) c= M ; :: thesis: verum