let r be Real; :: 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 st
( 0 < g & N = ].(r - g),(r + g).[ ) & |.(r - r).| = 0 ) by Def6, ABSVALUE:2;
hence r in N by Th1; :: thesis: verum