let x, a be Real; :: thesis: ex r being Real st
( 0 < r & x in ].(a - r),(a + r).[ )
consider r being Real such that
A1: |.(x - a).| < r by XREAL_1:1;
take r ; :: thesis: ( 0 < r & x in ].(a - r),(a + r).[ )
thus 0 < r by A1; :: thesis: x in ].(a - r),(a + r).[
thus x in ].(a - r),(a + r).[ by A1, RCOMP_1:1; :: thesis: verum