let V be non empty CLSStruct ; :: thesis: for M being Subset of V st M is Affine holds
M is convex
let M be Subset of V; :: thesis: ( M is Affine implies M is convex )
assume A1: M is Affine ; :: 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 A2: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M & v in M ) ; :: thesis: (z * u) + ((1r - z) * v) in M
then consider r being Real such that
A3: ( z = r & 0 < r & r < 1 ) ;
set s = 1r - z;
( 1 - r is Real & 1r - z = 1 - r ) by A3;
then ((1r - (1r - z)) * u) + ((1r - z) * v) in M by A1, A2, Def101;
hence (z * u) + ((1r - z) * v) in M ; :: thesis: verum