theorem :: SRINGS_5:77
for r, s, x being Real holds
( x in [.r,s.] iff 1 |-> x in ClosedHyperInterval (<*r*>,<*s*>) )