let V be RealLinearSpace; :: thesis: for B being Subset of V holds
( B is convex iff for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B )
let B be Subset of V; :: thesis: ( B is convex iff for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B )
thus ( B is convex implies for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) :: thesis: ( ( for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) implies B is convex )

proof

assume A1: B is convex ; :: thesis: for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B
for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B

proof

let x, y be Point of V; :: thesis: for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B
let r be Real; :: thesis: ( 0 <= r & r <= 1 & x in B & y in B implies (r * x) + ((1 - r) * y) in B )
assume that
A2: ( 0 <= r & r <= 1 ) and
A3: ( x in B & y in B ) ; :: thesis: (r * x) + ((1 - r) * y) in B
((1 - r) * y) + (r * x) in { (((1 - r1) * y) + (r1 * x)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by A2;
then A4: ((1 - r) * y) + (r * x) in LSeg (x,y) by RLTOPSP1:def 2;
LSeg (x,y) c= B by A1, A3, JORDAN1:def 1;
hence (r * x) + ((1 - r) * y) in B by A4; :: thesis: verum

end;

hence for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ; :: thesis: verum

end;

( ( for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) implies B is convex )

proof

assume A5: for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ; :: thesis: B is convex
for x, y being Point of V st x in B & y in B holds
LSeg (x,y) c= B

proof

let x, y be Point of V; :: thesis: ( x in B & y in B implies LSeg (x,y) c= B )
assume A6: ( x in B & y in B ) ; :: thesis: LSeg (x,y) c= B
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in LSeg (x,y) or p in B )
assume p in LSeg (x,y) ; :: thesis: p in B
then p in { (((1 - r1) * y) + (r1 * x)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RLTOPSP1:def 2;
then ex r1 being Real st
( p = ((1 - r1) * y) + (r1 * x) & 0 <= r1 & r1 <= 1 ) ;
hence p in B by A5, A6; :: thesis: verum

end;

hence B is convex by RLTOPSP1:22; :: thesis: verum

end;

hence ( ( for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) implies B is convex ) ; :: thesis: verum