theorem :: RCOMP_1:16

for r being Real
for N being Neighbourhood of r holds r in N