let V be non empty RLSStruct ; :: thesis: for M being cone Subset of V st V is RealLinearSpace-like 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 RealLinearSpace-like implies ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds
u + v in M ) )
assume A1: V is RealLinearSpace-like ; :: thesis: ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds
u + v in M )
A2: ( 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 A3: 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 A3, CONVEX1:def 2;
then A4: 2 * (((1 / 2) * u) + ((1 / 2) * v)) in M by Def3;
2 * (((1 / 2) * u) + ((1 / 2) * v)) = (2 * ((1 / 2) * u)) + (2 * ((1 / 2) * v)) by A1, RLVECT_1:def 9
.= ((2 * (1 / 2)) * u) + (2 * ((1 / 2) * v)) by A1, RLVECT_1:def 9
.= (1 * u) + ((2 * (1 / 2)) * v) by A1, RLVECT_1:def 9
.= u + (1 * v) by A1, RLVECT_1:def 9 ;
hence u + v in M by A1, A4, RLVECT_1:def 9; :: 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;

( ( 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 A5: 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
A6: ( 0 < r & r < 1 ) and
A7: ( u in M & v in M ) ; :: thesis: (r * u) + ((1 - r) * v) in M
r + 0 < 1 by A6;
then 1 - r > 0 by XREAL_1:22;
then ( r * u in M & (1 - r) * v in M ) by A6, A7, Def3;
hence (r * u) + ((1 - r) * v) in M by A5; :: thesis: verum

end;

hence M is convex by CONVEX1:def 2; :: 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 A2; :: thesis: verum