for a, b being ExtReal holds
( min (a,b) = a or min (a,b) = b ) by Def8;