let f be Relation; :: thesis:
thus ( dom f is complex-membered implies f is COMPLEX -defined ) :: thesis:

set E = (dom f) \/ COMPLEX;
reconsider X = dom f as Subset of ((dom f) \/ COMPLEX) by XBOOLE_1:7;
reconsider Y = COMPLEX as Subset of ((dom f) \/ COMPLEX) by XBOOLE_1:7;
assume dom f is complex-membered ; :: thesis:
then for x being Element of (dom f) \/ COMPLEX st x in dom f holds
x in COMPLEX by XCMPLX_0:def 2;
then X c= Y by SUBSET_1:2;
hence f is COMPLEX -defined by RELAT_1:def 18; :: thesis:

end;

thus ( f is COMPLEX -defined implies dom f is complex-membered ) ; :: thesis: