:: deftheorem Def9 defines max XXREAL_0:def 10 :
for a, b being ExtReal holds
( ( b <= a implies max (a,b) = a ) & ( not b <= a implies max (a,b) = b ) );