:: deftheorem defines add-closed MEMBERED:def 25 :
for X being set holds
( X is add-closed iff for x, y being Complex st x in X & y in X holds
x + y in X );