for n being Nat
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r )