theorem Th1: :: XXREAL_1:1

for r, s, t being ExtReal holds
( t in [.r,s.] iff ( r <= t & t <= s ) )