theorem :: XXREAL_0:15

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