theorem :: CONVEX4:74

for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : Im (u .|. v) >= r } holds
M is convex