theorem :: SRINGS_5:79

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