theorem Th7: :: MESFUN16:7

for I being closed_interval Subset of REAL
for E being Subset of RNS_Real st I = E holds
E is compact