let x be Point of R^1; :: thesis: for N being Subset of REAL
for M being Subset of R^1 st M = N & N is Neighbourhood of x holds
M is a_neighborhood of x
let N be Subset of REAL; :: thesis: for M being Subset of R^1 st M = N & N is Neighbourhood of x holds
M is a_neighborhood of x
let M be Subset of R^1; :: thesis: ( M = N & N is Neighbourhood of x implies M is a_neighborhood of x )
assume A1: M = N ; :: thesis: ( not N is Neighbourhood of x or M is a_neighborhood of x )
given r being Real such that A2: 0 < r and
A3: N = ].(x - r),(x + r).[ ; :: according to RCOMP_1:def 6 :: thesis: M is a_neighborhood of x
M is open by A1, A3, JORDAN6:35;
hence M is a_neighborhood of x by A1, A2, A3, CONNSP_2:3, TOPREAL6:15; :: thesis: verum