for s being Real st s > 0 holds
ex n being Element of NAT st
( n > 0 & 0 < 1 / n & 1 / n <= s )