for r being Real st r is irrational holds
( cocf r is convergent & lim (cocf r) = r )