let V be non empty RLSStruct ; :: thesis: for M being Subset of V holds

( M is convex iff for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M )

let M be Subset of V; :: thesis: ( M is convex iff for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M )

thus ( M is convex implies for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M ) :: thesis: ( ( for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M ) implies M is convex )

(r * M) + ((1 - r) * M) c= M ; :: 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 ( 0 < r & r < 1 ) ; :: thesis: ( not u in M or not v in M or (r * u) + ((1 - r) * v) in M )

then A6: (r * M) + ((1 - r) * M) c= M by A5;

assume ( u in M & v in M ) ; :: thesis: (r * u) + ((1 - r) * v) in M

then ( r * u in r * M & (1 - r) * v in { ((1 - r) * w) where w is Element of V : w in M } ) ;

then (r * u) + ((1 - r) * v) in { (p + q) where p, q is Element of V : ( p in r * M & q in (1 - r) * M ) } ;

then (r * u) + ((1 - r) * v) in (r * M) + ((1 - r) * M) by RUSUB_4:def 9;

hence (r * u) + ((1 - r) * v) in M by A6; :: thesis: verum

( M is convex iff for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M )

let M be Subset of V; :: thesis: ( M is convex iff for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M )

thus ( M is convex implies for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M ) :: thesis: ( ( for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M ) implies M is convex )

proof

assume A5:
for r being Real st 0 < r & r < 1 holds
assume A1:
M is convex
; :: thesis: for r being Real st 0 < r & r < 1 holds

(r * M) + ((1 - r) * M) c= M

let r be Real; :: thesis: ( 0 < r & r < 1 implies (r * M) + ((1 - r) * M) c= M )

assume A2: ( 0 < r & r < 1 ) ; :: thesis: (r * M) + ((1 - r) * M) c= M

for x being Element of V st x in (r * M) + ((1 - r) * M) holds

x in M

end;(r * M) + ((1 - r) * M) c= M

let r be Real; :: thesis: ( 0 < r & r < 1 implies (r * M) + ((1 - r) * M) c= M )

assume A2: ( 0 < r & r < 1 ) ; :: thesis: (r * M) + ((1 - r) * M) c= M

for x being Element of V st x in (r * M) + ((1 - r) * M) holds

x in M

proof

hence
(r * M) + ((1 - r) * M) c= M
; :: thesis: verum
let x be Element of V; :: thesis: ( x in (r * M) + ((1 - r) * M) implies x in M )

assume x in (r * M) + ((1 - r) * M) ; :: thesis: x in M

then x in { (u + v) where u, v is Element of V : ( u in r * M & v in (1 - r) * M ) } by RUSUB_4:def 9;

then consider u, v being Element of V such that

A3: x = u + v and

A4: ( u in r * M & v in (1 - r) * M ) ;

( ex w1 being Element of V st

( u = r * w1 & w1 in M ) & ex w2 being Element of V st

( v = (1 - r) * w2 & w2 in M ) ) by A4;

hence x in M by A1, A2, A3; :: thesis: verum

end;assume x in (r * M) + ((1 - r) * M) ; :: thesis: x in M

then x in { (u + v) where u, v is Element of V : ( u in r * M & v in (1 - r) * M ) } by RUSUB_4:def 9;

then consider u, v being Element of V such that

A3: x = u + v and

A4: ( u in r * M & v in (1 - r) * M ) ;

( ex w1 being Element of V st

( u = r * w1 & w1 in M ) & ex w2 being Element of V st

( v = (1 - r) * w2 & w2 in M ) ) by A4;

hence x in M by A1, A2, A3; :: thesis: verum

(r * M) + ((1 - r) * M) c= M ; :: 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 ( 0 < r & r < 1 ) ; :: thesis: ( not u in M or not v in M or (r * u) + ((1 - r) * v) in M )

then A6: (r * M) + ((1 - r) * M) c= M by A5;

assume ( u in M & v in M ) ; :: thesis: (r * u) + ((1 - r) * v) in M

then ( r * u in r * M & (1 - r) * v in { ((1 - r) * w) where w is Element of V : w in M } ) ;

then (r * u) + ((1 - r) * v) in { (p + q) where p, q is Element of V : ( p in r * M & q in (1 - r) * M ) } ;

then (r * u) + ((1 - r) * v) in (r * M) + ((1 - r) * M) by RUSUB_4:def 9;

hence (r * u) + ((1 - r) * v) in M by A6; :: thesis: verum