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