theorem Th3: :: XXREAL_1:3

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