let A be Neighbourhood of r; :: thesis: A is open
ex g being Real st
( 0 < g & A = ].(r - g),(r + g).[ ) by Def6;
hence A is open ; :: thesis: verum