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 and
A3: r <= 1 and
A4: u in M and
A5: 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, A3, 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, A4, A5, CONVEX1:def 2; :: thesis: verum

end;

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

then A7: r * u = 0. V by RLVECT_1:23;
(1 - r) * v = v by A6, RLVECT_1:def 9;
hence (r * u) + ((1 - r) * v) in M by A5, A7, RLVECT_1:def 7; :: thesis: verum

end;

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

then A9: (1 - r) * v = 0. V by RLVECT_1:23;
r * u = u by A8, RLVECT_1:def 9;
hence (r * u) + ((1 - r) * v) in M by A4, A9, RLVECT_1:def 7; :: thesis: verum

end;

end;

end;

assume A10: 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 Element of REAL 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 A10; :: thesis: verum