let X be set ; :: thesis: ( X is Subset of REAL implies X is Subset of ExtREAL )
assume A1: X is Subset of REAL ; :: thesis: X is Subset of ExtREAL
bool REAL c= bool ExtREAL by NUMBERS:31, ZFMISC_1:67;
hence X is Subset of ExtREAL by A1; :: thesis: verum