theorem :: XXREAL_0:21
for a, b, c being ExtReal st a < b & a < c holds
a < min (b,c) by Def8;