let R be Relation; :: thesis: ( R is ExtREAL -valued implies R is ext-real-valued )
assume R is ExtREAL -valued ; :: thesis: R is ext-real-valued
hence rng R c= ExtREAL by RELAT_1:def 19; :: according to VALUED_0:def 2 :: thesis: verum