rng (X --> x) c= REAL by MEMBERED:3;
hence X --> x is real-valued by Def3; :: thesis: verum