theorem :: XXREAL_2:13

for x being ExtReal holds min {x} = x by Lm2;