theorem :: XXREAL_0:50

for a, b being ExtReal st a <= min (a,b) holds
min (a,b) = a