A1: {x} c= ExtREAL by MEMBERED:2;
rng (X --> x) c= ExtREAL by A1, XBOOLE_1:1;
hence X --> x is ext-real-valued by Def2; :: thesis: verum