let x be Point of R^1; for M being a_neighborhood of x ex N being Neighbourhood of x st N c= M
let M be a_neighborhood of x; ex N being Neighbourhood of x st N c= M
consider V being Subset of R^1 such that
A1:
V is open
and
A2:
V c= M
and
A3:
x in V
by CONNSP_2:6;
consider r being Real such that
A4:
r > 0
and
A5:
].(x - r),(x + r).[ c= V
by A1, A3, FRECHET:8;
reconsider N = ].(x - r),(x + r).[ as Neighbourhood of x by A4, RCOMP_1:def 6;
take
N
; N c= M
thus
N c= M
by A2, A5; verum