:: deftheorem defines complex-containing NOMIN_4:def 1 :
for A being set holds
( A is complex-containing iff COMPLEX c= A );