let r, s, t be ExtReal; :: thesis: ( t in [.r,s.[ iff ( r <= t & t < s ) )

hereby :: thesis: ( r <= t & t < s implies t in [.r,s.[ )

assume t in [.r,s.[ ; :: thesis: ( r <= t & t < s )
then ex a being Element of ExtREAL st
( a = t & r <= a & a < s ) ;
hence ( r <= t & t < s ) ; :: thesis: verum

end;

t is Element of ExtREAL by XXREAL_0:def 1;
hence ( r <= t & t < s implies t in [.r,s.[ ) ; :: thesis: verum