theorem :: XXREAL_0:42

for a being ExtReal holds min (a,+infty) = a