for Exy being ExtReal holds {Exy} is Subset of ExtREAL by XXREAL_0:def 1, ZFMISC_1:31;