let X be RealLinearSpace; 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; ( 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 ( ( for u, w being Point of X st u in M & w in M holds
LSeg (u,w) c= M ) implies M is convex )
end;
assume A3:
for w, u being Point of X st w in M & u in M holds
LSeg (w,u) c= M
; M is convex
let u, w be Point of X; RLTOPSP1:def 1 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; ( 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 )
; (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; verum