let R be Relation; :: thesis: ( R is natural-valued implies R is ext-natural-valued )
assume R is natural-valued ; :: thesis: R is ext-natural-valued
then rng R c< ExtNAT by Th1, VALUED_0:def 6, XBOOLE_1:59;
hence R is ext-natural-valued by XBOOLE_0:def 8; :: thesis: verum