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