theorem Th85: :: XXREAL_1:85
for r, s being ExtReal st s <= r holds
( [.r,s.] c= {r} & [.r,s.] c= {s} )