let a, b be ext-real number ; :: thesis: min ((max (a,b)),b) = b
b <= max (a,b) by Th25;
hence min ((max (a,b)),b) = b by Def9; :: thesis: verum