theorem :: XXREAL_0:24

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