for a, b being ExtReal holds max ((min (a,b)),b) = b by Th17, Def9;