let R be Relation of Z,X; :: thesis: R is ext-natural-valued
( rng R c= X & X c= ExtNAT ) by ThSubset;
hence R is ext-natural-valued ; :: thesis: verum