theorem :: XXREAL_0:20

for a, b, c being ExtReal st a <= b & a <= c holds
a <= min (b,c) by Def8;