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