theorem :: MESFUN16:16

for H being Subset of RNS_Real
for I being open_interval Subset of REAL st H = I holds
H is open