rng (X --> x) c= ExtREAL by MEMBERED:2;
hence X --> x is ext-real-valued by Def2; :: thesis: verum