let a, b be ext-real number ; :: thesis: a <= max a,b
( a <= b or not a <= b ) ;
hence a <= max a,b by Def9; :: thesis: verum