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