theorem :: XREAL_1:228

for r, s, t being ExtReal st r < s & ( for q being ExtReal st r < q & q < s holds
t <= q ) holds
t <= r