rng (X --> x) c= INT by MEMBERED:5;
hence X --> x is INT -valued by RELAT_1:def 19; :: thesis: verum