set x = the Element of X;
F . the Element of X in rng F by FUNCT_2:4;
hence proj2 F is non empty Subset of ExtREAL by XBOOLE_1:1; :: thesis: verum