theorem :: SRINGS_5:80

for r, s, x being Real holds
( x in [.r,s.[ iff 1 |-> x in RightOpenHyperInterval (<*r*>,<*s*>) )