for A being non empty Subset of REAL
for x being Real
for y being R_eal st x = y & 0 <= y holds
inf (x ** A) = y * (inf A)