theorem :: XXREAL_2:11

for x being ExtReal holds max {x} = x by Lm1;