for Y being non empty Subset of ExtREAL
for r being R_eal st r in REAL holds
inf ({r} + Y) = (inf {r}) + (inf Y)