for r being Real ex n being Element of NAT st r <= n