:: deftheorem defines convex CONVEX4:def 23 :
for V being non empty CLSStruct
for M being Subset of V holds
( M is convex iff for u, v being VECTOR of V
for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M & v in M holds
(z * u) + ((1r - z) * v) in M );