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