rng F c= ExtREAL ;
hence rng F is non empty Subset of ExtREAL ; :: thesis: verum