theorem :: SRINGS_5:41

for n being non zero Nat
for x being object st x in MeasurableRectangle (ProductRightOpenIntervals 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.[ ) )