for X being complex-membered set st ( for c being Complex holds c in X ) holds
X = COMPLEX