theorem Th7: :: MESFUN17:7

for A being Subset of [:RNS_Real,RNS_Real,RNS_Real:] st A is open holds
A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))