let V be non empty RLSStruct ; :: thesis: for M being cone Subset of V st V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital holds
( M is convex iff for u, v being VECTOR of V st u in M & v in M holds
u + v in M )
let M be cone Subset of V; :: thesis: ( V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital implies ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds
u + v in M ) )
A1: ( ( for u, v being VECTOR of V st u in M & v in M holds
u + v in M ) implies M is convex )

proof

assume A2: for u, v being VECTOR of V st u in M & v in M holds
u + v in M ; :: thesis: M is convex
for u, v being VECTOR of V
for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M

proof

let u, v be VECTOR of V; :: 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
A3: 0 < r and
A4: r < 1 and
A5: u in M and
A6: v in M ; :: thesis: (r * u) + ((1 - r) * v) in M
reconsider r = r as Real ;
r + 0 < 1 by A4;
then 1 - r > 0 by XREAL_1:20;
then A7: (1 - r) * v in M by A6, Def3;
r * u in M by A3, A5, Def3;
hence (r * u) + ((1 - r) * v) in M by A2, A7; :: thesis: verum

end;

hence M is convex by CONVEX1:def 2; :: thesis: verum

end;

assume A8: ( V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital ) ; :: thesis: ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds
u + v in M )
( M is convex implies for u, v being VECTOR of V st u in M & v in M holds
u + v in M )

proof

assume A9: M is convex ; :: thesis: for u, v being VECTOR of V st u in M & v in M holds
u + v in M
for u, v being VECTOR of V st u in M & v in M holds
u + v in M

proof

let u, v be VECTOR of V; :: thesis: ( u in M & v in M implies u + v in M )
assume ( u in M & v in M ) ; :: thesis: u + v in M
then ((1 / 2) * u) + ((1 - (1 / 2)) * v) in M by A9, CONVEX1:def 2;
then A10: 2 * ((jd * u) + (jd * v)) in M by Def3;
2 * (((1 / 2) * u) + ((1 / 2) * v)) = (2 * ((1 / 2) * u)) + (2 * ((1 / 2) * v)) by A8, RLVECT_1:def 5
.= ((2 * (1 / 2)) * u) + (2 * ((1 / 2) * v)) by A8, RLVECT_1:def 7
.= (1 * u) + ((2 * (1 / 2)) * v) by A8, RLVECT_1:def 7
.= u + (1 * v) by A8, RLVECT_1:def 8 ;
hence u + v in M by A8, A10, RLVECT_1:def 8; :: thesis: verum

end;

hence for u, v being VECTOR of V st u in M & v in M holds
u + v in M ; :: thesis: verum

end;

hence ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds
u + v in M ) by A1; :: thesis: verum