:: deftheorem Def8 defines min XXREAL_0:def 9 :
for a, b being ExtReal holds
( ( a <= b implies min (a,b) = a ) & ( not a <= b implies min (a,b) = b ) );