:: deftheorem Def2 defines complex XCMPLX_0:def 2 :
for c being Number holds
( c is complex iff c in COMPLEX );