theorem Th9: :: MESFUN16:9

for I, J being closed_interval Subset of REAL
for E being Subset of [:RNS_Real,RNS_Real:] st E = [:I,J:] holds
E is compact