theorem :: SRINGS_5:35

for n being non zero Nat
for x being object st x in MeasurableRectangle (ProductLeftOpenIntervals n) holds
ex y being Subset of (REAL n) st
( x = y & ( for i being Nat st i in Seg n holds
ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] ) )