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