:: deftheorem Def3 defines real-valued VALUED_0:def 3 :
for f being Relation holds
( f is real-valued iff rng f c= REAL );