theorem Th18: :: RCOMP_1:18

for X being open Subset of REAL
for r being Real st r in X holds
ex N being Neighbourhood of r st N c= X