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