theorem :: XREAL_1:229

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