let V be non empty RLSStruct ; :: 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 CONVEX1:def 2 :: 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
0 < r and
r < 1 and
A2: ( u in M & v in M ) ; :: thesis: (r * u) + ((1 - r) * v) in M
set p = 1 - r;
1 - (1 - r) = r ;
hence (r * u) + ((1 - r) * v) in M by A1, A2, RUSUB_4:def 4; :: thesis: verum