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