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 that
A2: ex r being Real st
( z = r & 0 < r & r < 1 ) and
A3: ( u in M & v in M ) ; :: thesis: (z * u) + ((1r - z) * v) in M
set s = 1r - z;
consider r being Real such that
A4: z = r and
0 < r and
r < 1 by A2;
1r - z = 1 - r by A4;
then ((1r - (1r - z)) * u) + ((1r - z) * v) in M by A1, A3;
hence (z * u) + ((1r - z) * v) in M ; :: thesis: verum