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
( ex g being real number st
( 0 < g & N = ].(r - g),(r + g).[ ) & abs (r - r) = 0 ) by Def7, ABSVALUE:2;
hence r in N by Th8; :: thesis: verum