theorem Th74: :: MATHMORP:74

for V being RealLinearSpace
for B being Subset of V holds
( B is convex iff for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B )