theorem :: FINANCE2:7

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