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

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