theorem :: SRINGS_5:44

for n being non zero Nat
for x being set st x in MeasurableRectangle (ProductRightOpenIntervals n) holds
ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ )