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

proof

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

end;

thus ( f is RAT -valued implies rng f is rational-membered ) ; :: thesis: verum