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 ;
then p1 - z < (z + e) - z by XREAL_1:14;
then A4: |.(p1 - z).| < e by ;
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 ; :: 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 ;
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 ;
then A7: 0 - (p1 - z) < 0 - (- e) by XREAL_1:15;
A8: p1 < z by ;
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 ; :: thesis: verum
end;
end;