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 number such that A2: 0 < r and
A3: N = ].(x - r),(x + r).[ ; :: according to RCOMP_1:def 7 :: thesis: M is a_neighborhood of x
M is open by A1, A3, JORDAN6:46;
hence M is a_neighborhood of x by A1, A2, A3, CONNSP_2:5, TOPREAL6:20; :: thesis: verum