for V being non empty Abelian CLSStruct
for M being Subset of V st M is convex holds
for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) holds
((1r - z) * M) + (z * M) c= M