theorem Th34: :: SRINGS_5:42

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 f being b₁ -element FinSequence of [:REAL,REAL:] st
( x = y & ( for t being Element of REAL n holds
( t in y iff for i being Nat st i in Seg n holds
t . i in [.((f /. i) `1),((f /. i) `2).[ ) ) )