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 A2: ( u in M & 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, Def1; :: thesis: verum

end;

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

end;

assume A3: 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
A4: ( 0 <= r & r <= 1 ) and
A5: ( u in M & w in M ) ; :: thesis: (r * u) + ((1 - r) * w) in M
A6: (r * u) + ((1 - r) * w) in LSeg w,u by A4;
LSeg w,u c= M by A3, A5;
hence (r * u) + ((1 - r) * w) in M by A6; :: thesis: verum