theorem Th32: :: SRINGS_5:37

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