theorem Th4: :: XXREAL_1:4

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