theorem Th35: :: SRINGS_5:43

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