let f be Relation; :: thesis: ( dom f is natural-membered iff f is NAT -defined )
thus ( dom f is natural-membered implies f is NAT -defined ) :: thesis: ( f is NAT -defined implies dom f is natural-membered )

proof

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

end;

thus ( f is NAT -defined implies dom f is natural-membered ) ; :: thesis: verum