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;

( 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 )
;

end;

suppose A3:
0 <= z
; :: thesis: ex q being Element of RAT st

( q <> 0 & |.(z - q).| < e )

( 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;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

suppose A5:
z < 0
; :: thesis: ex q being Element of RAT st

( q <> 0 & |.(z - q).| < e )

( 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;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