let a, b be ext-real number ; :: thesis: ( max a,b <= a implies max a,b = a )
assume max a,b <= a ; :: thesis: max a,b = a
then ( max a,b < a or max a,b = a ) by Th1;
hence max a,b = a by Th25; :: thesis: verum