let r be real number ; :: thesis: for N being Neighbourhood of r holds r in N
let N be Neighbourhood of r; :: thesis: r in N
A1: ex g being real number st
( 0 < g & N = ].(r - g),(r + g).[ ) by Def7;
abs (r - r) = 0 by ABSVALUE:7;
hence r in N by A1, Th8; :: thesis: verum