theorem Th2: :: XXREAL_1:2

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