let a, b be ExtReal; :: thesis: a <= max (a,b)
( a <= b or not a <= b ) ;
hence a <= max (a,b) by Def9; :: thesis: verum