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

proof

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

end;

thus ( f is RAT -defined implies dom f is rational-membered ) ; :: thesis: verum