:: deftheorem Def2 defines ext-real-valued VALUED_0:def 2 :
for f being Relation holds
( f is ext-real-valued iff rng f c= ExtREAL );