theorem :: FRECHET:36

for r being Real st r > 0 holds
ex n being Nat st
( 1 / n < r & n > 0 ) by Lm1;