:: deftheorem Def3r defines rational-valued VALUED_0:def 4 :
for f being Relation holds
( f is rational-valued iff rng f c= RAT );