theorem Th21: :: NORMSP_4:16
for z, e being Real st 0 < e holds
ex q being Element of RAT st
( q <> 0 & |.(z - q).| < e )