theorem Th31: :: SRINGS_5:36

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 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).] ) ) )