let V be non empty CLSStruct ; :: thesis: for M being Subset of V holds
( M is convex iff for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
(z * M) + ((1r - z) * M) c= M )
let M be Subset of V; :: thesis: ( M is convex iff for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
(z * M) + ((1r - z) * M) c= M )
A1: ( M is convex implies for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
(z * M) + ((1r - z) * M) c= M )

proof

assume A2: M is convex ; :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
(z * M) + ((1r - z) * M) c= M
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) implies (z * M) + ((1r - z) * M) c= M )
assume A3: ex r being Real st
( z = r & 0 < r & r < 1 ) ; :: thesis: (z * M) + ((1r - z) * M) c= M
for x being Element of V st x in (z * M) + ((1r - z) * M) holds
x in M

proof

let x be Element of V; :: thesis: ( x in (z * M) + ((1r - z) * M) implies x in M )
assume x in (z * M) + ((1r - z) * M) ; :: thesis: x in M
then consider u, v being Element of V such that
A4: x = u + v and
A5: ( u in z * M & v in (1r - z) * M ) ;
( ex w1 being Element of V st
( u = z * w1 & w1 in M ) & ex w2 being Element of V st
( v = (1r - z) * w2 & w2 in M ) ) by A5;
hence x in M by A2, A3, A4; :: thesis: verum

end;

hence (z * M) + ((1r - z) * M) c= M ; :: thesis: verum

end;

( ( for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
(z * M) + ((1r - z) * M) c= M ) implies M is convex )

proof

assume A6: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
(z * M) + ((1r - z) * M) c= M ; :: thesis: M is convex
let u, v be VECTOR of V; :: according to CONVEX4:def 23 :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M & v in M holds
(z * u) + ((1r - z) * v) in M
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M & v in M implies (z * u) + ((1r - z) * v) in M )
assume ex r being Real st
( z = r & 0 < r & r < 1 ) ; :: thesis: ( not u in M or not v in M or (z * u) + ((1r - z) * v) in M )
then A7: (z * M) + ((1r - z) * M) c= M by A6;
assume ( u in M & v in M ) ; :: thesis: (z * u) + ((1r - z) * v) in M
then ( z * u in z * M & (1r - z) * v in (1r - z) * M ) ;
then (z * u) + ((1r - z) * v) in (z * M) + ((1r - z) * M) ;
hence (z * u) + ((1r - z) * v) in M by A7; :: thesis: verum

end;

hence ( M is convex iff for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
(z * M) + ((1r - z) * M) c= M ) by A1; :: thesis: verum