let z, e be Real; :: thesis: ( 0 < e implies ex q being Element of RAT st
( q <> 0 & |.(z - q).| < e ) )
assume A1: 0 < e ; :: thesis: ex q being Element of RAT st
( q <> 0 & |.(z - q).| < e )
then 0 + z < z + e by XREAL_1:8;
then consider p1, p2 being Rational such that
A2: ( z < p1 & p1 < p2 & p2 < z + e ) by BORSUK_5:26;

per cases ( 0 <= z or z < 0 ) ;

suppose A3: 0 <= z ; :: thesis: ex q being Element of RAT st
( q <> 0 & |.(z - q).| < e )

p1 < z + e by A2, XXREAL_0:2;
then p1 - z < (z + e) - z by XREAL_1:14;
then A4: |.(p1 - z).| < e by ABSVALUE:def 1, A2, XREAL_1:48;
reconsider p1 = p1 as Element of RAT by RAT_1:def 2;
take p1 ; :: thesis: ( p1 <> 0 & |.(z - p1).| < e )
thus p1 <> 0 by A2, A3; :: thesis: |.(z - p1).| < e
thus |.(z - p1).| < e by A4, COMPLEX1:60; :: thesis: verum

end;

suppose A5: z < 0 ; :: thesis: ex q being Element of RAT st
( q <> 0 & |.(z - q).| < e )

z - e < z - 0 by A1, XREAL_1:15;
then consider p1, p2 being Rational such that
A6: ( z - e < p1 & p1 < p2 & p2 < z ) by BORSUK_5:26;
(z - e) - z < p1 - z by A6, XREAL_1:14;
then A7: 0 - (p1 - z) < 0 - (- e) by XREAL_1:15;
A8: p1 < z by A6, XXREAL_0:2;
reconsider p1 = p1 as Element of RAT by RAT_1:def 2;
take p1 ; :: thesis: ( p1 <> 0 & |.(z - p1).| < e )
thus p1 <> 0 by A5, A6; :: thesis: |.(z - p1).| < e
thus |.(z - p1).| < e by A7, A8, ABSVALUE:def 1, XREAL_1:48; :: thesis: verum

end;

end;