theorem :: XXREAL_0:35

for a, b being ExtReal holds min ((max (a,b)),b) = b by Th25, Def8;