let a, b be ExtReal; :: 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