let X be RealLinearSpace; :: thesis: for M being Subset of X holds
( M is convex iff for u, w being Point of X st u in M & w in M holds
LSeg u,w c= M )
let M be Subset of X; :: thesis: ( M is convex iff for u, w being Point of X st u in M & w in M holds
LSeg u,w c= M )

hereby :: thesis: ( ( for u, w being Point of X st u in M & w in M holds
LSeg u,w c= M ) implies M is convex )

assume A1: M is convex ; :: thesis: for u, w being Point of X st u in M & w in M holds
LSeg u,w c= M
let u, w be Point of X; :: thesis: ( u in M & w in M implies LSeg u,w c= M )
assume that
A2: u in M and
A3: w in M ; :: thesis: LSeg u,w c= M

now

let x be set ; :: thesis: ( x in LSeg u,w implies x in M )
assume x in LSeg u,w ; :: thesis: x in M
then ex r being Real st
( x = ((1 - r) * u) + (r * w) & 0 <= r & r <= 1 ) ;
hence x in M by A1, A2, A3, Def1; :: thesis: verum

end;

hence LSeg u,w c= M by TARSKI:def 3; :: thesis: verum

end;

assume A4: for w, u being Point of X st w in M & u in M holds
LSeg w,u c= M ; :: thesis: M is convex
let u, w be Point of X; :: according to RLTOPSP1:def 1 :: thesis: for r being Real st 0 <= r & r <= 1 & u in M & w in M holds
(r * u) + ((1 - r) * w) in M
let r be Real; :: thesis: ( 0 <= r & r <= 1 & u in M & w in M implies (r * u) + ((1 - r) * w) in M )
assume that
A5: ( 0 <= r & r <= 1 ) and
A6: u in M and
A7: w in M ; :: thesis: (r * u) + ((1 - r) * w) in M
A8: (r * u) + ((1 - r) * w) in LSeg w,u by A5;
LSeg w,u c= M by A4, A6, A7;
hence (r * u) + ((1 - r) * w) in M by A8; :: thesis: verum