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