hereby :: thesis: ( ( for u, v being Point of V
for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M ) implies M is convex )

assume A1: M is convex ; :: thesis: for u, v being Point of V
for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(b₆ * b₄) + ((1 - b₆) * b₅) in M
let u, v be Point of V; :: thesis: for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(b₄ * b₂) + ((1 - b₄) * b₃) in M
let r be Real; :: thesis: ( 0 <= r & r <= 1 & u in M & v in M implies (b₃ * b₁) + ((1 - b₃) * b₂) in M )
assume that
A2: ( 0 <= r & r <= 1 ) and
A3: u in M and
A4: v in M ; :: thesis: (b₃ * b₁) + ((1 - b₃) * b₂) in M

per cases ( ( 0 < r & r < 1 ) or 0 = r or r = 1 ) by A2, XXREAL_0:1;

suppose ( 0 < r & r < 1 ) ; :: thesis: (b₃ * b₁) + ((1 - b₃) * b₂) in M

hence (r * u) + ((1 - r) * v) in M by A1, A3, A4; :: thesis: verum

end;

suppose 0 = r ; :: thesis: (b₃ * b₁) + ((1 - b₃) * b₂) in M

then ( r * u = 0. V & (1 - r) * v = v ) by RLVECT_1:10, RLVECT_1:def 8;
hence (r * u) + ((1 - r) * v) in M by A4; :: thesis: verum

end;

suppose r = 1 ; :: thesis: (b₃ * b₁) + ((1 - b₃) * b₂) in M

then ( (1 - r) * v = 0. V & r * u = u ) by RLVECT_1:10, RLVECT_1:def 8;
hence (r * u) + ((1 - r) * v) in M by A3; :: thesis: verum

end;

end;

end;

assume A5: for u, v being Point of V
for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M ; :: thesis: M is convex
let u, v be Point of V; :: according to CONVEX1:def 2 :: thesis: for b₁ being object holds
( b₁ <= 0 or 1 <= b₁ or not u in M or not v in M or (b₁ * u) + ((1 - b₁) * v) in M )
let r be Real; :: thesis: ( r <= 0 or 1 <= r or not u in M or not v in M or (r * u) + ((1 - r) * v) in M )
thus ( r <= 0 or 1 <= r or not u in M or not v in M or (r * u) + ((1 - r) * v) in M ) by A5; :: thesis: verum