theorem Th4: :: MESFUN17:4

for I, J, K being Interval holds
( [:[:I,J:],K:] is Subset of [:[:RNS_Real,RNS_Real:],RNS_Real:] & [:[:I,J:],K:] in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) )