let V be non empty Abelian RLSStruct ; :: thesis: for M being Subset of V st M is convex holds

for r being Real st 0 < r & r < 1 holds

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

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

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

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

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

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

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

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

x in M

for r being Real st 0 < r & r < 1 holds

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

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

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

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

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

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

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

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

x in M

proof

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

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

then x in { (u + v) where u, v is Element of V : ( u in (1 - r) * M & v in 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 (1 - r) * M & v in r * M ) ;

( ex w1 being Element of V st

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

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

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

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

then x in { (u + v) where u, v is Element of V : ( u in (1 - r) * M & v in 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 (1 - r) * M & v in r * M ) ;

( ex w1 being Element of V st

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

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

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