let X be open Subset of REAL; :: thesis: for r being real number st r in X holds
ex g being real number st
( 0 < g & ].(r - g),(r + g).[ c= X )
let r be real number ; :: thesis: ( r in X implies ex g being real number st
( 0 < g & ].(r - g),(r + g).[ c= X ) )
assume r in X ; :: thesis: ex g being real number st
( 0 < g & ].(r - g),(r + g).[ c= X )
then consider N being Neighbourhood of r such that
A1: N c= X by Th39;
consider g being real number such that
A2: ( 0 < g & N = ].(r - g),(r + g).[ ) by Def7;
take g ; :: thesis: ( 0 < g & ].(r - g),(r + g).[ c= X )
thus ( 0 < g & ].(r - g),(r + g).[ c= X ) by A1, A2; :: thesis: verum